le_inducedOuterMeasure — Mathlib

English

Under hs, the induced outer measure on s equals extend m s; a variant of the equality with different hypotheses.

Русский

При hs индуцированная внешняя мера на s равна extend m s; вариант формулы с иными предпосылками.

LaTeX

$$$\\mathrm{inducedOuterMeasure}\\ m P0 m0\\ s = \\mathrm{extend}\\ m\\ s$$$

Lean4

theorem le_inducedOuterMeasure {μ : OuterMeasure α} :
    μ ≤ inducedOuterMeasure m P0 m0 ↔ ∀ (s) (hs : P s), μ s ≤ m s hs :=
  le_ofFunction.trans <| forall_congr' fun _s => le_iInf_iff

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