diophFn_comp1 — Mathlib

English

If S is Dioph and f is DiophPFun, then the set {v | f(v) ::ₒ v ∈ S} is Dioph.

Русский

Если S диагофантово, а f — диагофантова частичная функция, то множество {v | f(v) :: v ∈ S} диагофантово.

LaTeX

$$$$\mathrm{Dioph}(S) \Rightarrow \mathrm{Dioph}\left(\{v : \alpha \to \mathbb{N} \mid \exists x: f.Dom(v), f.fn(v,x) ::_◦ v ∈ S\}\right)$$$$

Lean4

theorem diophFn_comp1 {S : Set (Option α → ℕ)} (d : Dioph S) {f : (α → ℕ) → ℕ} (df : DiophFn f) :
    Dioph {v | f v ::ₒ v ∈ S} :=
  ext (diophPFun_comp1 d <| cast (diophFn_iff_pFun f) df) fun _ => ⟨fun ⟨_, h⟩ => h, fun h => ⟨trivial, h⟩⟩

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