Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ceiling Unicode version

Definition df-ceiling 28254
Description: The ceiling function. Defined in ISO 80000-2:2009(E) operation 2-9.18 and the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4.

By convention metamath users tend to expand this construct directly, instead of using the definition. However, we want to make sure this is separately and formally defined. Proof ceicl 10955 shows that the ceiling function returns an integer when provided a real. Formalized by David A. Wheeler. (Contributed by David A. Wheeler, 19-May-2015.)

Assertion
Ref Expression
df-ceiling  |- =  ( x  e.  RR  |->  -u ( |_ `  -u x
) )

Detailed syntax breakdown of Definition df-ceiling
StepHypRef Expression
1 ccei 28253 . 2  class
2 vx . . 3  set  x
3 cr 8736 . . 3  class  RR
42cv 1622 . . . . . 6  class  x
54cneg 9038 . . . . 5  class  -u x
6 cfl 10924 . . . . 5  class  |_
75, 6cfv 5255 . . . 4  class  ( |_
`  -u x )
87cneg 9038 . . 3  class  -u ( |_ `  -u x )
92, 3, 8cmpt 4077 . 2  class  ( x  e.  RR  |->  -u ( |_ `  -u x ) )
101, 9wceq 1623 1  wff =  ( x  e.  RR  |->  -u ( |_ `  -u x
) )
Colors of variables: wff set class
This definition is referenced by:  ceilingval  28255
  Copyright terms: Public domain W3C validator