coe_toFinset

Mathlib.Data.List.Cycle

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

English

The coercion of a list to a cycle, then taking toFinset, yields the same as the list toFinset.

Русский

Переход списка в цикл, затем взятие toFinset даёт тот же результат, что и прямой toFinset списка.

LaTeX

$$$\big( (l : List\, \alpha) \big).toFinset = l.toFinset$$$

Lean4

@[simp]
theorem coe_toFinset (l : List α) : (l : Cycle α).toFinset = l.toFinset :=
  rfl

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

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

Разделы

Аффилиация

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