essInf_measure_zero — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\operatorname{essInf} f (0 : \\mathrm{Measure} \\alpha) = \\top $$$$

Lean4

@[simp]
theorem essInf_measure_zero {_ : MeasurableSpace α} {f : α → β} : essInf f (0 : Measure α) = ⊤ :=
  @essSup_measure_zero α βᵒᵈ _ _ _

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