Theorem essSup_le_of_ae_le

Modification history

2026-05-14 06:13
Mathlib/MeasureTheory/Function/EssSup.lean
feat(MeasureTheory): generalize some lemmas about essSup to conditionally complete lattices (#39104) …
Modified essSup_le_of_ae_leView on Github →
2023-11-10 17:28
Mathlib/MeasureTheory/Function/EssSup.lean
feat(LiminfLimsup, LpSeminorm): add lemmas/golf (#8300) …
Modified essSup_le_of_ae_leView on Github →
2023-05-21 14:20
Mathlib/MeasureTheory/Function/EssSup.lean
feat: port MeasureTheory.Function.EssSup (#4098)
Added essSup_le_of_ae_leView on Github →