ofEquiv — Mathlib

English

Equivalence of Primrec with Nat.Primrec via encoding for denumerable domains.

Русский

Эквивалентность Primrec и Nat.Primrec через кодирование для денумерируемых множеств.

LaTeX

$$$$\\text{Primrec } f \\leftrightarrow \\text{Nat.Primrec } n \\mapsto \\text{encode}(f(\\text{ofNat } \\alpha\\, n)).$$$$

Lean4

/-- Builds a `Primcodable` instance from an equivalence to a `Primcodable` type. -/
def ofEquiv (α) {β} [Primcodable α] (e : β ≃ α) : Primcodable β :=
  { __ := Encodable.ofEquiv α e
    prim :=
      (Primcodable.prim α).of_eq fun n => by
        rw [decode_ofEquiv]
        cases (@decode α _ n) <;> simp [encode_ofEquiv] }

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