ofFunction_apply — Mathlib

English

If m is monotone and sigma-subadditive, then the assembled outer measure equals m for all sets.

Русский

Если m монотонно по включениям и удовлетворяет сигма-субаддитивности, тогда собранная внешняя мера равна m для всех множеств.

LaTeX

$$$\\text{If } m\\text{ is monotone and sigma-subadditive, then } \\operatorname{OuterMeasure.ofFunction} m m\\_empty = m.$$$

Lean4

/-- `ofFunction` of a set `s` is the infimum of `∑ᵢ, m (tᵢ)` for all collections of sets
`tᵢ` that cover `s`. -/
theorem ofFunction_apply (s : Set α) :
    OuterMeasure.ofFunction m m_empty s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, m (t n) :=
  rfl

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