of_equiv_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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