English
Let C be a collection of sets whose generated sigma-algebra equals the ambient one, and B a function into sets with hA: generateFrom C equals the ambient sigma-algebra, and C is a π-system. If the union over i of B_i is univ, each B_i ∈ C, μ(B_i) is finite, and μ(s) = ν(s) for all s ∈ C, then μ = ν.
Русский
Пусть C образует порождающую сигма-алгебру π-система, B_i — элементы C, ⋃ B_i = α, каждый μ(B_i) конечно, и μ(s)=ν(s) для всех s∈C. Тогда μ=ν.
LaTeX
$$$μ = ν$ under the hypotheses that $C$ is a π-system with $generateFrom C = \\mathcal{F}$, $B_i\\in C$, $\\bigcup_i B_i = α$, $μ(B_i)\\neq \\infty$, and $μ(s)=ν(s)$ for all $s\\in C$.$$
Lean4
/-- Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on an increasing spanning sequence of sets in the π-system.
This lemma is formulated using `iUnion`.
`FiniteSpanningSetsIn.ext` is a reformulation of this lemma. -/
theorem ext_of_generateFrom_of_iUnion (C : Set (Set α)) (B : ℕ → Set α) (hA : ‹_› = generateFrom C) (hC : IsPiSystem C)
(h1B : ⋃ i, B i = univ) (h2B : ∀ i, B i ∈ C) (hμB : ∀ i, μ (B i) ≠ ∞) (h_eq : ∀ s ∈ C, μ s = ν s) : μ = ν :=
by
refine ext_of_generateFrom_of_cover_subset hA hC ?_ (countable_range B) h1B ?_ h_eq
· rintro _ ⟨i, rfl⟩
apply h2B
· rintro _ ⟨i, rfl⟩
apply hμB
