English
Let μ and ν be measures on α. Suppose S is a π-system that generates the σ-algebra on α, and T is a countable collection of sets such that the σ-algebra is generated by S and the union of T is the whole space. If μ and ν agree on all intersections of S with T (i.e., μ(s ∩ t) = ν(s ∩ t) for all s ∈ S, t ∈ T), and μ and ν assign the same finite values μ(t) = ν(t) to every t ∈ T, then μ = ν.
Русский
Пусть μ и ν — меры на α. Пусть S образует π-систему, порождающую сигма-алгебру на α, а T — счётное семейство множеств так, что сигма-алгебра порождается S и ⋃ T = α. Если μ и ν совпадают на всех пересечениях S ∩ t (для любых s ∈ S, t ∈ T), и μ(t) = ν(t) для всех t ∈ T, то μ = ν.
LaTeX
$$$\\mu = ν$ under the assumptions that $S$ is a $\\pi$-system with $S$ generating the $\\sigma$-algebra, $T$ is countable with $\\bigcup T = \\mathsf{univ}$, $\\forall t\\in T,\\mu(t)\\neq\\infty$, $\\forall t\\in T,\\forall s\\in S,\\mu(s\\cap t)=\\nu(s\\cap t)$, and $\\forall t\\in T,\\mu(t)=\\nu(t)$.$$
Lean4
theorem ext_of_generateFrom_of_cover {S T : Set (Set α)} (h_gen : ‹_› = generateFrom S) (hc : T.Countable)
(h_inter : IsPiSystem S) (hU : ⋃₀ T = univ) (htop : ∀ t ∈ T, μ t ≠ ∞)
(ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)) (T_eq : ∀ t ∈ T, μ t = ν t) : μ = ν :=
by
refine ext_of_sUnion_eq_univ hc hU fun t ht => ?_
ext1 u hu
simp only [restrict_apply hu]
induction u, hu using induction_on_inter h_gen h_inter with
| empty => simp only [Set.empty_inter, measure_empty]
| basic u hu => exact ST_eq _ ht _ hu
| compl u hu ihu =>
have := T_eq t ht
rw [Set.inter_comm] at ihu ⊢
rwa [← measure_inter_add_diff t hu, ← measure_inter_add_diff t hu, ← ihu, ENNReal.add_right_inj] at this
exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)
| iUnion f hfd hfm
ihf =>
simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢
simp only [measure_iUnion hfd hfm, ihf]
