Metamath Proof Explorer


Definition df-ceil

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

Detailed syntax breakdown

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