ofNat_of_decode

Mathlib.Logic.Denumerable

URI: https://scilib.ai/kg/mathlib#Denumerable.ofNat_of_decode

English

If decode α n = some b, then ofNat α n = b.

Русский

Если decode α n = some b, то ofNat α n = b.

LaTeX

$$$ decode\ (\alpha := \alpha)\ n = \text{Some } b \Rightarrow \ text{ofNat } α n = b $$$

Lean4

theorem ofNat_of_decode {n b} (h : decode (α := α) n = some b) : ofNat (α := α) n = b := by simpa using h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru