English
For countable ι, with s i subsets and μ, ν measures, μ|_{⋃ i} = ν|_{⋃ i} iff ∀ i, μ|_{s i} = ν|_{s i}.
Русский
Для счётного индекса ι: μ|_{⋃ i} = ν|_{⋃ i} тогда и только тогда, когда ∀ i, μ|_{s_i} = ν|_{s_i}.
LaTeX
$$$[Countable\, ι] \ (\forall i, μ.restrict (s i) = ν.restrict (s i)) \iff μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i)$$$
Lean4
theorem restrict_iUnion_congr [Countable ι] {s : ι → Set α} :
μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) ↔ ∀ i, μ.restrict (s i) = ν.restrict (s i) :=
by
refine ⟨fun h i => restrict_congr_mono (subset_iUnion _ _) h, fun h => ?_⟩
ext1 t ht
have D : Directed (· ⊆ ·) fun t : Finset ι => ⋃ i ∈ t, s i :=
Monotone.directed_le fun t₁ t₂ ht => biUnion_subset_biUnion_left ht
rw [iUnion_eq_iUnion_finset]
simp only [restrict_iUnion_apply_eq_iSup D ht, restrict_biUnion_finset_congr.2 fun i _ => h i]
