isCountablySpanning_spanningSets — Mathlib

English

Let μ be a sigma-finite measure on α. Then the family of spanning sets {spanningSets(μ, n)} (as n runs over the natural numbers) forms a countable spanning family, i.e. their union covers the whole space.

Русский

Пусть μ — сигма-ограниченная мера на α. Тогда семейство покрывающих множеств {spanningSets(μ, n)} при n ∈ ℕ образует счетное покрытие, то есть их объединение охватывает всю область.

LaTeX

$$$\bigcup_{n\in\mathbb{N}} spanningSets(\mu,n) = \mathrm{univ}_{\alpha}$$$

Lean4

theorem isCountablySpanning_spanningSets (μ : Measure α) [SigmaFinite μ] :
    IsCountablySpanning (range (spanningSets μ)) :=
  ⟨spanningSets μ, mem_range_self, iUnion_spanningSets μ⟩

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