English
Deleting the first component preserves Diophantine property: the projection on the tail of a Diophantine set remains Diophantine.
Русский
Удаление первого компонента сохраняет диагофантовость: проекция на хвост остается диагофантовой.
LaTeX
$$$$\mathrm{Dioph}\left(\{v: Fin2(n) \to \mathbb{N} \mid \exists x, (x :: v) \in S\}\right)$$$$
Lean4
/-- Deleting the first component preserves the Diophantine property. -/
theorem vec_ex1_dioph (n) {S : Set (Vector3 ℕ (succ n))} (d : Dioph S) : Dioph {v : Fin2 n → ℕ | ∃ x, (x :: v) ∈ S} :=
ext (ex1_dioph <| reindex_dioph _ (none :: some) d) fun v =>
exists_congr fun x => by
dsimp
rw [show Option.elim' x v ∘ cons none some = x :: v from funext fun s => by rcases s with a | b <;> rfl]
