Commit 2023-05-10 00:18 13d7a9c2

View on Github →

feat: port MeasureTheory.Lattice (#3824)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Lattice.lean

added theorem AEMeasurable.const_inf

added theorem AEMeasurable.const_sup

added theorem AEMeasurable.inf'

added theorem AEMeasurable.inf

added theorem AEMeasurable.inf_const

added theorem AEMeasurable.sup'

added theorem AEMeasurable.sup

added theorem AEMeasurable.sup_const

added theorem Finset.measurable_range_sup''

added theorem Finset.measurable_range_sup'

added theorem Finset.measurable_sup'

added theorem Measurable.const_inf

added theorem Measurable.const_sup

added theorem Measurable.inf'

added theorem Measurable.inf

added theorem Measurable.inf_const

added theorem Measurable.sup'

added theorem Measurable.sup

added theorem Measurable.sup_const