mem_support_notMem_vars_zero — Mathlib

English

As a simplification, i ∈ p.vars iff ∃ d ∈ p.support with i ∈ d.support.

Русский

Упрощенно: i ∈ p.vars эквивалентно существованию d ∈ p.support such that i ∈ d.support.

LaTeX

$$$$ i \in p.\mathrm{vars} \Leftrightarrow \exists d \in p.\mathrm{support},\ i \in d.\mathrm{support} $$$$

Lean4

theorem mem_support_notMem_vars_zero {f : MvPolynomial σ R} {x : σ →₀ ℕ} (H : x ∈ f.support) {v : σ} (h : v ∉ vars f) :
    x v = 0 := by
  contrapose! h
  exact (mem_vars v).mpr ⟨x, H, Finsupp.mem_support_iff.mpr h⟩

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