Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-24 16:02 ed2ab1a3

View on Github →

feat(measure_theory): measures form a complete lattice

Estimated changes

Modified src/data/set/basic.lean

added theorem set.empty_diff

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.measure.Inf_apply

added theorem measure_theory.measure.Inf_caratheodory

Modified src/measure_theory/outer_measure.lean

added theorem measure_theory.outer_measure.Inf_eq_of_function_Inf_gen

added def measure_theory.outer_measure.Inf_gen

added theorem measure_theory.outer_measure.Inf_gen_empty

added theorem measure_theory.outer_measure.Inf_gen_nonempty1

added theorem measure_theory.outer_measure.Inf_gen_nonempty2

added theorem measure_theory.outer_measure.top_caratheodory