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 | ⊢ ⌈ = ( 𝑥 ∈ ℝ ↦ - ( ⌊ ‘ - 𝑥 ) ) |