forall_iff_forall_finsupp — Mathlib

English

A polynomial property P is equivalent to the corresponding property on AddMonoidAlgebra via toFinsupp.

Русский

Свойство P о полиномах эквивалентно соответствующему свойству на AddMonoidAlgebra через преобразование toFinsupp.

LaTeX

$$$ \forall P : (Polynomial\ R \to Prop), \Big( (\forall p, P(p)) \iff (\forall q : R[\mathbb{N}], P(\{ toFinsupp := q \})) \Big) $$$

Lean4

theorem forall_iff_forall_finsupp (P : R[X] → Prop) : (∀ p, P p) ↔ ∀ q : R[ℕ], P ⟨q⟩ :=
  ⟨fun h q => h ⟨q⟩, fun h ⟨p⟩ => h p⟩

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