essSup_measure_zero — Mathlib

English

Let β be a complete lattice. For every function f: α → β, the essential supremum of f with respect to the zero measure on α equals the bottom element ⊥ of β.

Русский

Пусть β — полная решётка. Для любой функции f: α → β эсс-супремум f по нулевой мере равен нижней грани ⊥ данной решётки.

LaTeX

$$$$ \\operatorname{essSup} f (0 : \\mathrm{Measure} \\alpha) = \\perp $$$$

Lean4

@[simp]
theorem essSup_measure_zero {m : MeasurableSpace α} {f : α → β} : essSup f (0 : Measure α) = ⊥ :=
  le_bot_iff.mp (sInf_le (by simp))

Похожие утверждения