mem_vars — Mathlib

English

For a polynomial p and index i, i is in p.vars iff there exists a degree d in p.support with i in d.support.

Русский

Для многочлена p и индекса i справедливо: i ∈ p.vars тогда и только тогда, когда существует компонент deg d ∈ p.support such that i ∈ d.support.

LaTeX

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

Lean4

theorem mem_vars (i : σ) : i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support := by
  classical simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff]

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