English
If S is Dioph, and f is a DiophPFun, then the set {v : α → ℕ | ∃ h : f.Dom v, f.fn v h ::ₒ v ∈ S} is Dioph.
Русский
Если S диагофантова, а f — диагофантова частичная функция, то множество {v | ∃h, ... } является диагофантовым.
LaTeX
$$$$\mathrm{Dioph}(S) \Rightarrow \mathrm{Dioph}\left(\{v : \alpha \to \mathbb{N} \mid \exists h: f.\mathrm{Dom}(v), f.f n(v,h) ::_◦ v \in S\}\right)$$$$
Lean4
theorem diophPFun_comp1 {S : Set (Option α → ℕ)} (d : Dioph S) {f} (df : DiophPFun f) :
Dioph {v : α → ℕ | ∃ h : f.Dom v, f.fn v h ::ₒ v ∈ S} :=
ext (ex1_dioph (d.inter df)) fun v =>
⟨fun ⟨x, hS, (h : Exists _)⟩ =>
by
rw [show (x ::ₒ v) ∘ some = v from funext fun s => rfl] at h
obtain ⟨hf, h⟩ := h; refine ⟨hf, ?_⟩; rw [PFun.fn, h]; exact hS, fun ⟨x, hS⟩ =>
⟨f.fn v x, hS, show Exists _ by rw [show (f.fn v x ::ₒ v) ∘ some = v from funext fun s => rfl]; exact ⟨x, rfl⟩⟩⟩
