English
Let μ and ν be measures on α. If S is a generating π-system, T ⊆ S is a subset that covers the same σ-algebra with ⋃ T = univ, T is countable, μ and ν are finite on every t ∈ T, and μ(s) = ν(s) for all s ∈ S, then μ = ν.
Русский
Пусть μ и ν — меры на α. Пусть S образует порождающую π-систему, T ⊆ S покрывает ту же сигма-алгебру и ⋃ T = univ, T счётно, μ(t) и ν(t) конечны для всех t ∈ T, и μ(s) = ν(s) для всех s ∈ S. Тогда μ = ν.
LaTeX
$$$\\mu = ν$ при условии, что $S$ порождает сигма-алгебру, $T \\subseteq S$, $T$ счётно, $\\bigcup T = \\mathrm{univ}$, $\\forall t\\in T,\\mu(t)\\neq\\infty$, $\\forall s\\in S,\\mu(s)=\\nu(s)$. \\\\ $\\Rightarrow\\ μ=ν$.$$
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 `sUnion`. -/
theorem ext_of_generateFrom_of_cover_subset {S T : Set (Set α)} (h_gen : ‹_› = generateFrom S) (h_inter : IsPiSystem S)
(h_sub : T ⊆ S) (hc : T.Countable) (hU : ⋃₀ T = univ) (htop : ∀ s ∈ T, μ s ≠ ∞) (h_eq : ∀ s ∈ S, μ s = ν s) :
μ = ν := by
refine ext_of_generateFrom_of_cover h_gen hc h_inter hU htop ?_ fun t ht => h_eq t (h_sub ht)
intro t ht s hs; rcases (s ∩ t).eq_empty_or_nonempty with H | H
· simp only [H, measure_empty]
· exact h_eq _ (h_inter _ hs _ (h_sub ht) H)
