English
If t is finite and the variable sets of φ_i are pairwise disjoint, then the variables of the sum ∑_{i∈t} φ_i equal the disjoint union of the individual variable sets; i.e., they equal the biUnion of the φ_i vars.
Русский
Если t конечное и множества переменных φ_i попарно неперекрываются, тогда множество переменных суммы ∑_{i∈t} φ_i равно непересекаемому объединению множеств переменных φ_i.
LaTeX
$$$ (\sum_{i \in t} \phi_i).vars = \mathrm{Finset.biUnion}_{i \in t} (\phi_i).vars $$$
Lean4
theorem vars_sum_of_disjoint [DecidableEq σ] (h : Pairwise <| (Disjoint on fun i => (φ i).vars)) :
(∑ i ∈ t, φ i).vars = Finset.biUnion t fun i => (φ i).vars := by
classical
induction t using Finset.induction_on with
| empty => simp
| insert _ _ has
hsum =>
rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
unfold Pairwise onFun at h
simp only [Finset.disjoint_iff_ne] at h ⊢
grind
