exists_iff_exists_finsupp — Mathlib

English

There exists a polynomial with property P if and only if there exists a finsupp representation q with P(⟨q⟩).

Русский

Существует полином с свойством P тогда и только тогда, когда существует представление через finsupp q с P(⟨q⟩).

LaTeX

$$$ \exists p, P(p) \\iff \exists q : R[\mathbb{N}], P(\langle q \rangle) $$$

Lean4

theorem exists_iff_exists_finsupp (P : R[X] → Prop) : (∃ p, P p) ↔ ∃ q : R[ℕ], P ⟨q⟩ :=
  ⟨fun ⟨⟨p⟩, hp⟩ => ⟨p, hp⟩, fun ⟨q, hq⟩ => ⟨⟨q⟩, hq⟩⟩

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