length_le_krullDim

Mathlib.Order.KrullDimension

URI: https://scilib.ai/kg/mathlib#Order.LTSeries.length_le_krullDim

English

For any LT-series p in α, the length p.length is bounded above by the Krull dimension of α.

Русский

Для любой LT-цепи p в α длина p.length ограничена сверху размером Клу-дель α.

LaTeX

$$$$ p.length \le \operatorname{krullDim}(\alpha) $$$$

Lean4

theorem length_le_krullDim (p : LTSeries α) : p.length ≤ krullDim α :=
  le_sSup ⟨_, rfl⟩

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

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

Разделы

Аффилиация

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