vars_eq_support_biUnion_support — Mathlib

English

Same as the disjoint sums case: under pairwise disjointness of variable sets, the variables of the sum equal the biUnion of variable sets.

Русский

То же самое, что и раньше в случае попарного непересечения множеств переменных: переменные суммы равны biUnion переменных членов.

LaTeX

$$$ (\sum_{i \in t} \phi_i).vars = \mathrm{Finset.biUnion}_{i \in t} (\phi_i).vars $$$

Lean4

theorem vars_eq_support_biUnion_support [DecidableEq σ] : p.vars = p.support.biUnion Finsupp.support :=
  by
  ext i
  rw [mem_vars, Finset.mem_biUnion]

Похожие утверждения