length_toList

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.length_toList

English

Let x be a RelSeries r. Then the length of its toList equals the length of x plus one.

Русский

Пусть x — RelSeries r. Тогда длина x.toList равна длине x плюс 1.

LaTeX

$$$|x.toList| = x.length + 1$$$

Lean4

@[simp]
theorem length_toList (x : RelSeries r) : x.toList.length = x.length + 1 :=
  List.length_ofFn

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

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

Разделы

Аффилиация

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