of_equiv — Mathlib

English

If e: β ≃ α is a bijection and α is Primcodable, then the corresponding map e: β → α is Primrec.

Русский

Если e: β ≃ α — биекция и α примкодируем, то соответствующая функция e: β → α примрrec.

LaTeX

$$$$ \\mathrm{Primrec}(e) \\text{ for } e: \\beta \\xrightarrow{\\sim} \\alpha \\text{ (a bijection)} $$$$

Lean4

theorem of_equiv {β} {e : β ≃ α} :
    haveI := Primcodable.ofEquiv α e
    Primrec e :=
  letI : Primcodable β := Primcodable.ofEquiv α e
  encode_iff.1 Primrec.encode

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