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