Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-19 07:58 2d935cbc

View on Github →

refactor(lebesgue_measure): clean up proofs

Estimated changes

Modified algebra/ordered_group.lean

added theorem lt_sub

deleted theorem lt_sub_iff

deleted theorem sub_lt_iff

Modified algebra/ordered_ring.lean

Modified analysis/ennreal.lean

Modified analysis/limits.lean

Modified analysis/measure_theory/lebesgue_measure.lean

modified theorem measure_theory.le_lebesgue_length

modified theorem measure_theory.lebesgue_Ico

modified theorem measure_theory.lebesgue_Ioo

added theorem measure_theory.lebesgue_length_Ico'

modified theorem measure_theory.lebesgue_length_Ico

deleted theorem measure_theory.lebesgue_length_Ico_le_lebesgue_length_Ico

modified theorem measure_theory.lebesgue_outer_Ico

Modified analysis/measure_theory/outer_measure.lean

added theorem measure_theory.outer_measure.of_function_le

Modified analysis/topology/topological_structures.lean

Modified data/int/basic.lean

Modified data/set/intervals.lean

added theorem set.Ico_sdiff_Ioo_eq_singleton

added theorem set.Ico_self

added theorem set.Ico_subset_Ico_left

added theorem set.Ico_subset_Ico_right

added theorem set.Ico_subset_Iio_self

added theorem set.Ico_subset_Ioo_left

added theorem set.Ioo_self

added theorem set.Ioo_subset_Ico_self