dom_dioph — Mathlib

English

The notion of a Diophantine partial function coincides with a Diophantine total function via a standard lifting, i.e., DiophPFun f and DiophFn f are equivalent representations.

Русский

Указание на то, что диофантова частичная функция эквивалентна диофантовой полной функции через стандартное отображение.

LaTeX

$$$$\mathrm{DiophPFun}(f) \iff \mathrm{DiophFn}(f)$$$$

Lean4

theorem dom_dioph {f : (α → ℕ) →. ℕ} (d : DiophPFun f) : Dioph f.Dom :=
  cast (congr_arg Dioph <| Set.ext fun _ => (PFun.dom_iff_graph _ _).symm) (ex1_dioph d)

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