Commit 2023-04-21 19:31 52932b3a
View on Github →chore(measure_theory/function/ess_sup): Generalise (#18669)
A handful of lemmas hold for bounded filters in conditionally complete lattices, rather than just filter in complete lattices (which are automatically bounded).
Also prove that μ {y | x < f y} = 0 when x is greater than the essential supremum of f, and dually.