English
If μ|_{⋃ i∈s} t_i = ν|_{⋃ i∈s} t_i for a countable s, then μ|_{t_i} = ν|_{t_i} for all i ∈ s.
Русский
Если μ ограничено на объединение по i в s равно ν ограничено на то же объединение, то для каждого i ∈ s следует μ|_{t_i} = ν|_{t_i}.
LaTeX
$$$s.Countable \implies (μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) \iff ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i))$$$
Lean4
theorem restrict_biUnion_finset_congr {s : Finset ι} {t : ι → Set α} :
μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i) := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert i s _ hs =>
simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
rw [restrict_union_congr, ← hs]