of_no_dummies — Mathlib

English

If S ⊆ α → ℕ is given by S v ↔ p v = 0 for some polynomial p, then Dioph S.

Русский

Если множество S задаётся existential через полином p так, что S v ↔ p v = 0, то S диофово.

LaTeX

$$$$ \\forall S \\; p, \\ (\\forall v, S(v) \\iff p(v) = 0) \\rightarrow \\text{Dioph} S $$$$

Lean4

theorem of_no_dummies (S : Set (α → ℕ)) (p : Poly α) (h : ∀ v, S v ↔ p v = 0) : Dioph S :=
  ⟨PEmpty, ⟨p.map inl, fun v => (h v).trans ⟨fun h => ⟨PEmpty.elim, h⟩, fun ⟨_, ht⟩ => ht⟩⟩⟩

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