nil_toFinset

Mathlib.Data.List.Cycle

URI: https://scilib.ai/kg/mathlib#Cycle.nil_toFinset

English

The empty list, when viewed as a cycle, has an empty Finset.

Русский

Пустой список, представленный как цикл, имеет пустое Finset.

LaTeX

$$$\big(@nil\, \alpha\big).toFinset = \emptyset$$$

Lean4

@[simp]
theorem nil_toFinset : (@nil α).toFinset = ∅ :=
  rfl

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

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

Разделы

Аффилиация

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