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 28508
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 10971 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 28507 . 2  class
2 vx . . 3  set  x
3 cr 8752 . . 3  class  RR
42cv 1631 . . . . . 6  class  x
54cneg 9054 . . . . 5  class  -u x
6 cfl 10940 . . . . 5  class  |_
75, 6cfv 5271 . . . 4  class  ( |_
`  -u x )
87cneg 9054 . . 3  class  -u ( |_ `  -u x )
92, 3, 8cmpt 4093 . 2  class  ( x  e.  RR  |->  -u ( |_ `  -u x ) )
101, 9wceq 1632 1  wff =  ( x  e.  RR  |->  -u ( |_ `  -u x
) )
Colors of variables: wff set class
This definition is referenced by:  ceilingval  28509
  Copyright terms: Public domain W3C validator