of_equiv_symm_iff — Mathlib

English

For e: β ≃ α and f: σ → α, the statement (Primrec (λ a, e.symm (f a))) is equivalent to Primrec f.

Русский

Для e: β ≃ α и f: σ → α, Primrec (λ a, e.symm(f(a))) эквивалентно Primrec f.

LaTeX

$$$$ \\mathrm{Primrec}(\\lambda a. e^{-1}(f(a))) \\iff \\mathrm{Primrec}(f) $$$$

Lean4

theorem of_equiv_symm_iff {β} (e : β ≃ α) {f : σ → α} :
    haveI := Primcodable.ofEquiv α e
    (Primrec fun a => e.symm (f a)) ↔ Primrec f :=
  letI := Primcodable.ofEquiv α e
  ⟨fun h => (of_equiv.comp h).of_eq fun a => by simp, of_equiv_symm.comp⟩

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