length_le_coheight_head

Mathlib.Order.KrullDimension

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

← MathLib Explorer

English

For any LTSeries p, p.length ≤ coheight(p.head).

Русский

Для любой LTSeries p, длина p ≤ coheight(p.head).

LaTeX

$$$p.length \le \operatorname{coheight}(p.head).$$$

Lean4

/-- The coheight of the first element in a series is larger or equal to the length of the series.
-/
theorem length_le_coheight_head {p : LTSeries α} : p.length ≤ coheight p.head :=
  length_le_coheight le_rfl

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

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

Разделы

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

Аффилиация

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