Commit 2023-09-07 11:10 c719310c

View on Github →

feat: sups and limsups are measurable in conditionally complete linear orders (#6979) Currently, we only have that sups and limsups are measurable in complete linear orders, which excludes the main case of the real line. With more complicated proofs, these measurability results can be extended to all conditionally complete linear orders, without any further assumption in the statements.

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.nonempty_iInter_Ici_iff

added theorem Set.nonempty_iInter_Iic_iff

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

modified theorem Measurable.iInf_Prop

modified theorem Measurable.iSup_Prop

added theorem Measurable.isGLB_of_mem

added theorem Measurable.isLUB_of_mem

added theorem measurableSet_bddAbove_range

added theorem measurableSet_bddBelow_range

deleted theorem measurable_cInf

deleted theorem measurable_cSup

deleted theorem measurable_ciInf

deleted theorem measurable_ciSup

modified theorem measurable_liminf'

added theorem measurable_sInf

added theorem measurable_sSup

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Filter.HasBasis.liminf_eq_ciSup_ciInf

added theorem Filter.HasBasis.liminf_eq_ite

added theorem Filter.HasBasis.liminf_eq_sSup_iUnion_iInter

added theorem Filter.HasBasis.liminf_eq_sSup_univ_of_empty

added theorem Filter.HasBasis.limsup_eq_ciInf_ciSup

added theorem Filter.HasBasis.limsup_eq_ite

added theorem Filter.HasBasis.limsup_eq_sInf_iUnion_iInter

added theorem Filter.HasBasis.limsup_eq_sInf_univ_of_empty

Modified Mathlib/Probability/Kernel/CondCdf.lean