Theorem essSup_mono_measure'

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

2023-08-10 19:52

Mathlib/MeasureTheory/Function/EssSup.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified essSup_mono_measure'View on Github →

2023-05-21 14:20

Mathlib/MeasureTheory/Function/EssSup.lean

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

Added essSup_mono_measure'View on Github →