Description: The ceiling (least integer greater than or equal to) 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 . See ceilval for its value, ceilge and ceilm1lt for its basic properties, and ceilcl for its closure. For example, ( |^( 3 / 2 ) ) = 2 while ( |^-u ( 3 / 2 ) ) = -u 1 ( ex-ceil ).
The symbol |^ is inspired by the gamma shaped left bracket of the usual notation. (Contributed by David A. Wheeler, 19-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-ceil | |- |^ = ( x e. RR |-> -u ( |_ ` -u x ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cceil | |- |^ |
|
| 1 | vx | |- x |
|
| 2 | cr | |- RR |
|
| 3 | cfl | |- |_ |
|
| 4 | 1 | cv | |- x |
| 5 | 4 | cneg | |- -u x |
| 6 | 5 3 | cfv | |- ( |_ ` -u x ) |
| 7 | 6 | cneg | |- -u ( |_ ` -u x ) |
| 8 | 1 2 7 | cmpt | |- ( x e. RR |-> -u ( |_ ` -u x ) ) |
| 9 | 0 8 | wceq | |- |^ = ( x e. RR |-> -u ( |_ ` -u x ) ) |