innerContent_iUnion_nat — Mathlib

English

The previous bound becomes an equality when you pass to the iSup over opens.

Русский

Предыдущее неравенство превращается в равенство при учёте iSup по открытым множествам.

LaTeX

$$$μ.innerContent( \bigcup_i U_i ) = \operatorname{isub} iSup_i μ.innerContent(U_i)$$$

Lean4

/-- The inner content of a union of sets is at most the sum of the individual inner contents.
  This is the "unbundled" version of `innerContent_iSup_nat`.
  It is required for the API of `inducedOuterMeasure`. -/
theorem innerContent_iUnion_nat [R1Space G] ⦃U : ℕ → Set G⦄ (hU : ∀ i : ℕ, IsOpen (U i)) :
    μ.innerContent ⟨⋃ i : ℕ, U i, isOpen_iUnion hU⟩ ≤ ∑' i : ℕ, μ.innerContent ⟨U i, hU i⟩ :=
  by
  have := μ.innerContent_iSup_nat fun i => ⟨U i, hU i⟩
  rwa [Opens.iSup_def] at this

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