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

Definition df-ceiling 28528
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 11233 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 28527 . 2  class
2 vx . . 3  set  x
3 cr 8990 . . 3  class  RR
42cv 1652 . . . . . 6  class  x
54cneg 9293 . . . . 5  class  -u x
6 cfl 11202 . . . . 5  class  |_
75, 6cfv 5455 . . . 4  class  ( |_
`  -u x )
87cneg 9293 . . 3  class  -u ( |_ `  -u x )
92, 3, 8cmpt 4267 . 2  class  ( x  e.  RR  |->  -u ( |_ `  -u x ) )
101, 9wceq 1653 1  wff =  ( x  e.  RR  |->  -u ( |_ `  -u x
) )
Colors of variables: wff set class
This definition is referenced by:  ceilingval  28529
  Copyright terms: Public domain W3C validator