Theorem essSup_mono_ae

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_mono_ae View on Github →

2023-05-21 14:20

Mathlib/MeasureTheory/Function/EssSup.lean

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

Added essSup_mono_ae View on Github →