isGreatest_ofFunction — Mathlib

English

The outer measure constructed by ofFunction is the greatest among all outer measures dominated by m.

Русский

Внешняя мера, построенная через ofFunction, является наибольшей среди всех внешних мер, ограниченных сверху m.

LaTeX

$$$IsGreatest\\{\\mu : OuterMeasure α \\mid \\forall s, \\mu s ≤ m s\\} (OuterMeasure.ofFunction m m\\_empty).$$$

Lean4

theorem isGreatest_ofFunction : IsGreatest {μ : OuterMeasure α | ∀ s, μ s ≤ m s} (OuterMeasure.ofFunction m m_empty) :=
  ⟨fun _ => ofFunction_le _, fun _ => le_ofFunction.2⟩

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