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.
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
