longestOf_is_longest — Mathlib

English

For α with FiniteDimensionalOrder, and any x in LTSeries α, we have x.length ≤ (LTSeries.longestOf α).length.

Русский

Пусть α имеет конечномерный порядок, тогда для любой цепочки LTSeries в α выполнено, что её длина не превосходит максимальной длины LTSeries.longestOf α.

LaTeX

$$$\forall \alpha\ [FiniteDimensionalOrder \alpha], \forall x:\ LTSeries\alpha, x.length \le (LTSeries.longestOf \alpha).length$$$

Lean4

theorem longestOf_is_longest [FiniteDimensionalOrder α] (x : LTSeries α) : x.length ≤ (LTSeries.longestOf α).length :=
  RelSeries.length_le_length_longestOf _ _

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