Commit 2024-08-16 08:13 a6b7481a

View on Github →

feat: Essential supremum according to the counting measure (#15403) ... is just the usual supremum From LeanAPAP

Estimated changes

Modified Mathlib/MeasureTheory/Function/EssSup.lean

added theorem essInf_count

added theorem essInf_eq_iInf

added theorem essSup_count

added theorem essSup_eq_iSup

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

added theorem MeasureTheory.eLpNormEssSup_count

added theorem MeasureTheory.eLpNormEssSup_eq_iSup

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

added theorem MeasureTheory.AEStronglyMeasurable.of_finite

Modified Mathlib/MeasureTheory/OuterMeasure/AE.lean

added theorem MeasureTheory.ae_eq_comm

modified theorem MeasureTheory.ae_eq_refl

added theorem MeasureTheory.ae_eq_rfl

added theorem MeasureTheory.ae_eq_top

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.eventuallyEq_comm

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Filter.liminf_top

added theorem Filter.limsup_top