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	$$⊢⌈.⌉=\left(x\in ℝ⟼-⌊-x⌋\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cceil	$$class⌈.⌉$$
1		vx	$$setvarx$$
2		cr	$$classℝ$$
3		cfl	$$class⌊.⌋$$
4	1	cv	$$setvarx$$
5	4	cneg	$$class\left(-x\right)$$
6	5 3	cfv	$$class⌊-x⌋$$
7	6	cneg	$$class\left(-⌊-x⌋\right)$$
8	1 2 7	cmpt	$$class\left(x\in ℝ⟼-⌊-x⌋\right)$$
9	0 8	wceq	$$wff⌈.⌉=\left(x\in ℝ⟼-⌊-x⌋\right)$$