vars_add_of_disjoint — Mathlib

English

If p.vars and q.vars are disjoint, then (p+q).vars equals p.vars ∪ q.vars.

Русский

Если p.vars и q.vars непересекаются, то (p+q).vars равно p.vars ∪ q.vars.

LaTeX

$$$$ \text{If } \mathrm{Disjoint}(p.\mathrm{vars}, q.\mathrm{vars}), \ (p+q).\mathrm{vars} = p.\mathrm{vars} \cup q.\mathrm{vars} $$$$

Lean4

theorem vars_add_of_disjoint [DecidableEq σ] (h : Disjoint p.vars q.vars) : (p + q).vars = p.vars ∪ q.vars :=
  by
  refine (vars_add_subset p q).antisymm fun x hx => ?_
  simp only [vars_def, Multiset.disjoint_toFinset] at h hx ⊢
  rwa [degrees_add_of_disjoint h, Multiset.toFinset_union]

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