Commit 2024-09-10 03:09 16981db3

View on Github →

feat: limsup u ⊤ = ⨆ i, u i in a conditionally complete lattice (#16135) From LeanAPAP

Estimated changes

Modified Mathlib/MeasureTheory/Function/EssSup.lean

Modified Mathlib/Order/CompleteLattice.lean

added theorem sInf_upperBounds_eq_csSup

added theorem sSup_lowerBounds_eq_sInf

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem csInf_upperBounds_eq_csSup

deleted theorem csInf_upper_bounds_eq_csSup

added theorem csSup_lowerBounds_eq_csInf

deleted theorem csSup_lower_bounds_eq_csInf

Modified Mathlib/Order/Filter/Basic.lean

modified theorem Filter.EventuallyEq.eventually

added theorem Filter.eventuallyEq_top

Modified Mathlib/Order/LiminfLimsup.lean

deleted theorem Filter.liminf_top

added theorem Filter.liminf_top_eq_ciInf

added theorem Filter.liminf_top_eq_iInf

deleted theorem Filter.limsInf_principal

added theorem Filter.limsInf_principal_eq_csSup

added theorem Filter.limsInf_principal_eq_sInf

deleted theorem Filter.limsSup_principal

added theorem Filter.limsSup_principal_eq_csSup

added theorem Filter.limsSup_principal_eq_sSup

deleted theorem Filter.limsup_top

added theorem Filter.limsup_top_eq_ciSup

added theorem Filter.limsup_top_eq_iSup