Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-12 01:48 01746f84

View on Github →

feat(outer_measure): define bounded_by (#5314) bounded_by wrapper around of_function that drops the condition that m ∅ = 0. Refactor Inf_gen to use bounded_by. I am also planning to use bounded_by for finitary products of measures. Also add some complete lattice lemmas

Estimated changes

Modified src/measure_theory/measure_space.lean

Modified src/measure_theory/outer_measure.lean

added theorem measure_theory.outer_measure.Inf_eq_bounded_by_Inf_gen

deleted theorem measure_theory.outer_measure.Inf_eq_of_function_Inf_gen

added theorem measure_theory.outer_measure.Inf_gen_def

deleted theorem measure_theory.outer_measure.Inf_gen_empty

deleted theorem measure_theory.outer_measure.Inf_gen_nonempty1

deleted theorem measure_theory.outer_measure.Inf_gen_nonempty2

added def measure_theory.outer_measure.bounded_by

added theorem measure_theory.outer_measure.bounded_by_apply

added theorem measure_theory.outer_measure.bounded_by_caratheodory

added theorem measure_theory.outer_measure.bounded_by_eq

added theorem measure_theory.outer_measure.bounded_by_eq_of_function

added theorem measure_theory.outer_measure.bounded_by_le

added theorem measure_theory.outer_measure.le_bounded_by'

added theorem measure_theory.outer_measure.le_bounded_by

added theorem measure_theory.outer_measure.supr_Inf_gen_nonempty

Modified src/order/complete_lattice.lean

added theorem binfi_le_of_le

added theorem le_bsupr_of_le

added theorem le_infi_const

added theorem supr_const_le