Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-16 05:29 d84dfb17

View on Github →

feat(data/real): completeness of the (new) real numbers

Estimated changes

Modified algebra/group.lean

deleted theorem le_sub_iff_add_le

added theorem sub_add_sub_cancel'

deleted theorem sub_le_iff_le_add

Modified algebra/ordered_field.lean

added theorem inv_le

deleted theorem inv_le_inv'

modified theorem inv_le_inv

added theorem inv_le_inv_of_le

added theorem inv_lt

added theorem le_inv

added theorem lt_inv

Modified algebra/ordered_group.lean

modified theorem le_neg_add_iff_add_le

added theorem le_sub

modified theorem le_sub_right_iff_add_le

modified theorem lt_sub_right_iff_add_lt

modified theorem sub_right_le_iff_le_add

modified theorem sub_right_lt_iff_lt_add

Modified algebra/ordered_ring.lean

added theorem sub_one_lt

Modified analysis/ennreal.lean

Modified analysis/measure_theory/lebesgue_measure.lean

Modified analysis/measure_theory/measurable_space.lean

Modified analysis/measure_theory/measure_space.lean

Modified analysis/metric_space.lean

Modified analysis/real.lean

Modified analysis/topology/topological_structures.lean

Modified data/int/basic.lean

added theorem int.add_one_le_iff

added theorem int.exists_greatest_of_bdd

added theorem int.exists_least_of_bdd

added theorem int.le_sub_one_iff

added theorem int.lt_add_one_iff

modified theorem int.of_nat_add_neg_succ_of_nat_of_ge

modified theorem int.of_nat_add_neg_succ_of_nat_of_lt

added theorem int.sub_one_le_iff

Modified data/int/order.lean

deleted theorem int.exists_greatest_of_bdd

deleted theorem int.exists_least_of_bdd

Modified data/pnat.lean

added theorem pnat.coe_nat_coe

Modified data/rat.lean

Modified data/real.lean

added theorem NEW.real.Inf_le

added theorem NEW.real.Sup_le

added theorem NEW.real.Sup_le_ub

added theorem NEW.real.ceil_add_int

added theorem NEW.real.ceil_coe

added theorem NEW.real.ceil_le

added theorem NEW.real.ceil_lt_add_one

added theorem NEW.real.ceil_mono

added theorem NEW.real.ceil_sub_int

added theorem NEW.real.exists_floor

added theorem NEW.real.exists_sup

added theorem NEW.real.floor_add_int

added theorem NEW.real.floor_coe

added theorem NEW.real.floor_le

added theorem NEW.real.floor_lt

added theorem NEW.real.floor_mono

added theorem NEW.real.floor_sub_int

added theorem NEW.real.lb_le_Inf

added theorem NEW.real.le_Inf

added theorem NEW.real.le_Sup

added theorem NEW.real.le_ceil

added theorem NEW.real.le_floor

added theorem NEW.real.le_mk_of_forall_le

added theorem NEW.real.lt_ceil

added theorem NEW.real.lt_floor_add_one

added theorem NEW.real.lt_succ_floor

added theorem NEW.real.mk_le_of_forall_le

added theorem NEW.real.sub_one_lt_floor