Theorem le_essInf_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 le_essInf_of_ae_le View on Github →

2023-05-21 14:20

Mathlib/MeasureTheory/Function/EssSup.lean

feat: port MeasureTheory.Function.EssSup (#4098)

Added le_essInf_of_ae_le View on Github →