ulower_up — Mathlib

English

For any primcodable α, the map α ↦ ULower.down(α) is primitive recursive.

Русский

Для любого примитивно-кодируемого α функция α ↦ ULower.down(α) является примитивно-рекурсивной.

LaTeX

$$$\mathrm{PR}(\mathrm{ULower}.\down : \alpha \to \mathrm{ULower}\alpha)$$$

Lean4

theorem ulower_up : Primrec (ULower.up : ULower α → α) :=
  letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidableRangeEncode _
  option_get (Primrec.decode₂.comp subtype_val)

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