mem_support_finSuccEquiv — Mathlib

English

The image of the support under thefinSuccEquiv mapping corresponds to a particular subset described via a Finset image of cons.

Русский

Образ опорирования через отображение finSuccEquiv сопоставляет заданный подмножество через образ Finset image от константы.

LaTeX

$$$\\operatorname{image\\_support\\_finSuccEquiv}\\;{f} : \\cdots$$$

Lean4

theorem mem_support_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {x} :
    x ∈ (finSuccEquiv R n f).support ↔ x ∈ (fun m : Fin (n + 1) →₀ _ ↦ m 0) '' f.support := by
  simpa using congr(x ∈ $(support_finSuccEquiv f))

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