Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-16 02:55 fe1ad4b0

View on Github →

feat(data/rat): derive properties of rat floor and ceil

Estimated changes

Modified data/int/basic.lean

added theorem int.le_to_nat

added theorem int.lt_succ_self

added theorem int.pred_self_lt

added theorem int.to_nat_eq_max

added theorem int.to_nat_le

Modified data/rat.lean

added theorem rat.ceil_add_int

added theorem rat.ceil_coe

added theorem rat.ceil_le

added theorem rat.ceil_mono

added theorem rat.ceil_sub_int

modified theorem rat.coe_int_add

modified theorem rat.coe_int_eq_mk

added theorem rat.coe_int_inj

added theorem rat.coe_int_le

added theorem rat.coe_int_lt

added theorem rat.coe_int_mul

added theorem rat.coe_int_neg

modified theorem rat.coe_int_one

modified theorem rat.coe_int_sub

modified theorem rat.coe_nat_rat_eq_mk

deleted theorem rat.exists_upper_nat_bound

added theorem rat.floor_add_int

added theorem rat.floor_coe

added theorem rat.floor_le

added theorem rat.floor_lt

added theorem rat.floor_mono

added theorem rat.floor_sub_int

added theorem rat.le_ceil

added theorem rat.le_floor

added theorem rat.le_nat_ceil

deleted theorem rat.le_of_of_int_le_of_int

added theorem rat.lt_nat_ceil

added theorem rat.lt_succ_floor

added theorem rat.mk_le

modified def rat.nat_ceil

added theorem rat.nat_ceil_add_nat

deleted theorem rat.nat_ceil_add_one_eq

added theorem rat.nat_ceil_coe

added theorem rat.nat_ceil_le

modified theorem rat.nat_ceil_lt_add_one

deleted theorem rat.nat_ceil_min

modified theorem rat.nat_ceil_mono

deleted theorem rat.nat_ceil_spec

modified theorem rat.nat_ceil_zero

added theorem rat.sub_def

Modified topology/real.lean