length_toList'

Mathlib.Data.Ordmap.Invariants

URI: https://scilib.ai/kg/mathlib#Ordnode.length_toList'

← MathLib Explorer

English

The length of toList(t) equals t.realSize for every t.

Русский

Длина списка toList(t) равна realSize(t) для любого t.

LaTeX

$$length(toList(t)) = realSize(t)$$

Lean4

theorem length_toList' : ∀ t : Ordnode α, (toList t).length = t.realSize
  | nil => rfl
  | node _ l _ r => by rw [toList_node, List.length_append, List.length_cons, length_toList' l, length_toList' r]; rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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