snd — Mathlib

English

The second projection from a product is primitive recursive: Prod.snd.

Русский

Вторая проекция из произведения примрrec: Prod.snd.

LaTeX

$$$$ \\mathrm{Primrec}(\\mathrm{Prod.snd}) $$$$

Lean4

theorem snd {α β} [Primcodable α] [Primcodable β] : Primrec (@Prod.snd α β) :=
  ((casesOn' zero
            ((casesOn' zero (Nat.Primrec.succ.comp right)).comp (pair right ((Primcodable.prim β).comp left)))).comp
        (pair right ((Primcodable.prim α).comp left))).of_eq
    fun n => by
    simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]
    cases @decode α _ n.unpair.1 <;> simp
    cases @decode β _ n.unpair.2 <;> simp

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