iUnion_spanningSets — Mathlib

English

For σ-finite μ, the union over i of spanningSets μ i equals the whole space: ⋃_{i} spanningSets μ i = univ.

Русский

Для σ-конечной μ объединение всех spanningSets μ i равно вселенной.

LaTeX

$$Set.iUnion (fun i => spanningSets μ i) = Set.univ$$

Lean4

@[simp]
theorem iUnion_spanningSets (μ : Measure α) [SigmaFinite μ] : ⋃ i : ℕ, spanningSets μ i = univ := by
  simp_rw [spanningSets, iUnion_accumulate, μ.toFiniteSpanningSetsIn.spanning]

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