list_ofNat_zero

Mathlib.Logic.Equiv.List

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

English

For any Denumerable α, List α equals ofNat (List α) 0 equals [].

Русский

Для денумерабельного α список List α равен пустому списку при нуле.

LaTeX

$$$\\text{list\_ofNat\_zero} : \\; ofNat (List \\alpha) 0 = []$$$

Lean4

@[simp]
theorem list_ofNat_zero : ofNat (List α) 0 = [] := by rw [← @encode_list_nil α, ofNat_encode]

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

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

Разделы

Аффилиация

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