decode₂_is_partial_inv

Mathlib.Logic.Encodable.Basic

URI: https://scilib.ai/kg/mathlib#Encodable.decode₂_is_partial_inv

English

The encoding and decoding functions form a partial inverse pair.

Русский

Кодирование и декодирование образуют частичную обратную пару.

LaTeX

$$$ \text{IsPartialInv}(\mathrm{encode}, \mathrm{decode}_2(\cdot))$$$

Lean4

theorem decode₂_is_partial_inv [Encodable α] : IsPartialInv encode (decode₂ α) := fun _ _ => mem_decode₂

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

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

Разделы

Аффилиация

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