ofNat_encode

Mathlib.Logic.Denumerable

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

English

Conversely, encoding an element a and then taking ofNat returns a: ofNat α (encode a) = a.

Русский

Напротив, кодирование элемента a с последующим взятием ofNat возвращает сам элемент: ofNat α (encode a) = a.

LaTeX

$$$ \text{ofNat} \ (\alpha) \ (\text{encode } a) = a $$$

Lean4

@[simp]
theorem ofNat_encode (a) : ofNat α (encode a) = a :=
  ofNat_of_decode (encodek _)

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

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

Разделы

Аффилиация

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