English
If f is a Diophantine partial function, then its domain f.Dom is Diophantine.
Русский
Если f — частная диофантова функция, то её область определения f.Dom является диагофантовой.
LaTeX
$$$$\mathrm{Dioph}(f.\mathrm{Dom})$$$$
Lean4
theorem ex1_dioph {S : Set (Option α → ℕ)} : Dioph S → Dioph {v | ∃ x, x ::ₒ v ∈ S}
| ⟨β, p, pe⟩ =>
⟨Option β, p.map (inr none ::ₒ inl ⊗ inr ∘ some), fun v =>
⟨fun ⟨x, hx⟩ =>
let ⟨t, ht⟩ := (pe _).1 hx
⟨x ::ₒ t, by
simp only [Poly.map_apply]
rw [show (v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = x ::ₒ v ⊗ t from
funext fun s => by
rcases s with a | b <;>
try { cases a <;> rfl
};
rfl]
exact ht⟩,
fun ⟨t, ht⟩ =>
⟨t none,
(pe _).2
⟨t ∘ some, by
simp only [Poly.map_apply] at ht
rwa [show (v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = t none ::ₒ v ⊗ t ∘ some from
funext fun s => by
rcases s with a | b <;>
try { cases a <;> rfl
};
rfl] at ht⟩⟩⟩⟩
