length_le_height_last

Mathlib.Order.KrullDimension

URI: https://scilib.ai/kg/mathlib#Order.length_le_height_last

← MathLib Explorer

English

For any LTSeries p, p.length ≤ height(p.last).

Русский

Для любой LTSeries p длина p ≤ height(p.last).

LaTeX

$$$p^{\text{length}} \le \operatorname{height}(p.last).$$$

Lean4

/-- The height of the last element in a series is larger or equal to the length of the series.
-/
theorem length_le_height_last {p : LTSeries α} : p.length ≤ height p.last :=
  length_le_height le_rfl

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

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

Разделы

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

Аффилиация

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