Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-23 16:03 162d060c

View on Github →

feat(measure_theory/function/strongly_measurable): more basic properties of strongly_measurable (#12164)

Estimated changes

Modified src/algebra/support.lean

added theorem function.support_const_smul_of_ne_zero

Modified src/measure_theory/constructions/borel_space.lean

added theorem measurable_of_tendsto_ennreal'

added theorem measurable_of_tendsto_ennreal

Modified src/measure_theory/function/strongly_measurable.lean

added theorem measure_theory.ae_fin_strongly_measurable.ae_eq_mk

added theorem measure_theory.ae_fin_strongly_measurable.fin_strongly_measurable_mk

added theorem measure_theory.ae_fin_strongly_measurable_zero

modified theorem measure_theory.fin_strongly_measurable.ae_fin_strongly_measurable

modified theorem measure_theory.fin_strongly_measurable.exists_set_sigma_finite

added theorem measure_theory.fin_strongly_measurable_zero

added theorem measure_theory.simple_func.strongly_measurable

modified def measure_theory.strongly_measurable.approx

added theorem measure_theory.strongly_measurable_const

added theorem measure_theory.strongly_measurable_id

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.simple_func.coe_inf

added theorem measure_theory.simple_func.coe_sup