fst — Mathlib

English

The first projection from a product is primitive recursive: Prod.fst.

Русский

Первая проекция из произведения примрrec: Prod.fst.

LaTeX

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

Lean4

theorem fst {α β} [Primcodable α] [Primcodable β] : Primrec (@Prod.fst α β) :=
  ((casesOn' zero
            ((casesOn' zero (Nat.Primrec.succ.comp left)).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

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