vars_pow — Mathlib

English

The variables of φ^n are contained in the variables of φ, for any n ≥ 0.

Русский

Переменные φ^n лежат внутри переменных φ для любого n ≥ 0.

LaTeX

$$$$ (\varphi^n).\mathrm{vars} \subseteq \varphi.\mathrm{vars} $$$$

Lean4

theorem vars_pow (φ : MvPolynomial σ R) (n : ℕ) : (φ ^ n).vars ⊆ φ.vars := by
  classical
    induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ']
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset (Finset.Subset.refl _) ih

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