vars_sub_of_disjoint — Mathlib

English

For p and q, the variables of p − q are contained in the union of the variables of p and q.

Русский

Переменные p − q ⊆ переменные p ∪ переменные q.

LaTeX

$$$\\mathrm{vars}(p - q) \\subseteq \\mathrm{vars}(p) \\cup \\mathrm{vars}(q)$$$

Lean4

@[simp]
theorem vars_sub_of_disjoint [DecidableEq σ] (hpq : Disjoint p.vars q.vars) : (p - q).vars = p.vars ∪ q.vars :=
  by
  rw [← vars_neg q] at hpq
  convert vars_add_of_disjoint hpq using 2 <;> simp [sub_eq_add_neg]

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