ofFunction_eq_sSup — Mathlib

English

Repeating the supremum characterization: the same supremum representation holds for the maximal outer measure.

Русский

Повторяем характеристику супремума: та же самая запись через супремум описывает наибольшую внешнюю меру.

LaTeX

$$$\\text{ofFunction}(m,m\\_empty) = sSup\\{\\mu : \\forall s, \\mu(s) ≤ m(s)\\}.$$$

Lean4

theorem ofFunction_eq_sSup : OuterMeasure.ofFunction m m_empty = sSup {μ | ∀ s, μ s ≤ m s} :=
  (@isGreatest_ofFunction α m m_empty).isLUB.sSup_eq.symm

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