sumInr — Mathlib

English

Let α and β be types with primitive encodings. The right injection Sum.inr : β → α ⊕ β is primitive recursive.

Русский

Пусть α и β — типы с примкодируемыми отображениями. Правая инъекция Sum.inr : β → α ⊕ β является примитивно вычислимой.

LaTeX

$$$\\mathrm{Primrec}(\\mathrm{Sum.inr})$$$

Lean4

theorem sumInr : Primrec (@Sum.inr α β) :=
  encode_iff.1 <| nat_double_succ.comp Primrec.encode

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