Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-20 20:02 42355947

View on Github →

feat(topology/outer_measure): add outer measures and tools for Caratheodorys extension method

Estimated changes

Modified algebra/field.lean

added theorem inv_pos

Modified algebra/ordered_monoid.lean

Modified data/finset/basic.lean

modified theorem finset.subset.refl

modified theorem finset.upto_succ

modified theorem finset.upto_zero

added theorem lt_max_iff

Modified data/set/lattice.lean

added theorem set.sdiff_subset_sdiff

added theorem set.subset_Union

Modified order/boolean_algebra.lean

added theorem lattice.sub_le_sub

Modified topology/ennreal.lean

added theorem Inf_lt_iff

added theorem ennreal.le_of_forall_epsilon_le

added theorem ennreal.lt_add_right

added theorem ennreal.sum_of_real

added theorem ennreal.supr_add

added theorem infi_lt_iff

deleted theorem inv_inv'

deleted theorem inv_pos

Modified topology/limits.lean

deleted theorem inv_pos

Modified topology/measure.lean

Created topology/outer_measure.lean

added theorem Inter_neg

added theorem Inter_pos

added theorem Inter_univ

added theorem Union_empty

added theorem Union_neg

added theorem Union_pos

added theorem classical.or_not

added theorem ennreal.add_infi

added theorem ennreal.infi_add

added theorem ennreal.infi_add_infi

added theorem ennreal.infi_sum

added theorem inv_lt_one

added def measure_theory.outer_measure.inf

added theorem measure_theory.outer_measure.inf_space_is_measurable

added def measure_theory.outer_measure.measure

added def measure_theory.outer_measure.space

added theorem measure_theory.outer_measure.space_is_measurable_eq

added theorem measure_theory.outer_measure.subadditive

added structure measure_theory.outer_measure

added theorem sdiff_empty

added theorem sdiff_eq:

added theorem union_sdiff_left

added theorem union_sdiff_right

Modified topology/real.lean

modified theorem one_lt_two