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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cceil | ||
1 | vx | ||
2 | cr | ||
3 | cfl | ||
4 | 1 | cv | |
5 | 4 | cneg | |
6 | 5 3 | cfv | |
7 | 6 | cneg | |
8 | 1 2 7 | cmpt | |
9 | 0 8 | wceq |