English
Let α be a type with FiniteDimensionalOrder. For p : LTSeries α, if every q : LTSeries α satisfies q.length ≤ p.length, then p.length = (LTSeries.longestOf α).length.
Русский
Пусть α обладает конечномерным порядком. Для p : LTSeries α, если каждый q : LTSeries α удовлетворяет q.length ≤ p.length, то p.length равно длине LTSeries.longestOf α.
LaTeX
$$$\forall \alpha\ [FiniteDimensionalOrder \alpha] (p: LTSeries\alpha) (is_longest: \forall q: LTSeries\alpha, q.length ≤ p.length), p.length = (LTSeries.longestOf \alpha).length$$$
Lean4
theorem longestOf_len_unique [FiniteDimensionalOrder α] (p : LTSeries α)
(is_longest : ∀ (q : LTSeries α), q.length ≤ p.length) : p.length = (LTSeries.longestOf α).length :=
le_antisymm (longestOf_is_longest _) (is_longest _)
