Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-03 15:41 2b3cffd3

View on Github →

feat(algebra/floor): notation for nat_floor and nat_ceil (#8526) We introduce the notations ⌊a⌋₊ for nat_floor a and ⌈a⌉₊ for nat_ceil a, mimicking the existing notations for floor and ceil (with the + corresponding to the recent notation for nnnorm).

Estimated changes

modified theorem ceil_eq_on_Ioc'
modified theorem ceil_eq_on_Ioc
modified theorem floor_eq_on_Ico'
modified theorem floor_eq_on_Ico
modified theorem int.preimage_Ici
modified theorem int.preimage_Iic
modified theorem int.preimage_Iio
modified theorem int.preimage_Ioi
modified theorem le_nat_ceil
modified theorem le_nat_floor_iff
modified theorem le_nat_floor_of_le
modified theorem le_of_nat_ceil_le
modified theorem lt_nat_ceil
modified theorem lt_nat_floor_add_one
modified theorem lt_of_lt_nat_floor
modified theorem lt_of_nat_ceil_lt
modified theorem nat_ceil_add_nat
modified theorem nat_ceil_coe
modified theorem nat_ceil_le
modified theorem nat_ceil_lt_add_one
modified theorem nat_ceil_mono
modified theorem nat_ceil_zero
modified theorem nat_floor_add_nat
modified theorem nat_floor_coe
modified theorem nat_floor_eq_zero_iff
modified theorem nat_floor_le
modified theorem nat_floor_lt_iff
modified theorem nat_floor_mono
modified theorem nat_floor_of_nonpos
modified theorem nat_floor_zero
modified theorem pos_of_nat_floor_pos