English
Equivalent expression for height using end-at-a series.
Русский
Эквивалентное выражение высоты через цепь, оканчивающуюся в a.
LaTeX
$$$\operatorname{height}(a) = \sup\{ \operatorname{length}(p) : p : LTSeries(\alpha), p.last = a \}. $$$
Lean4
/-- Alternative definition of height, with the supremum ranging only over those series that end at `a`.
-/
theorem height_eq_iSup_last_eq (a : α) : height a = ⨆ (p : LTSeries α) (_ : p.last = a), ↑(p.length) :=
by
apply eq_of_forall_ge_iff
intro n
rw [height_le_iff', iSup₂_le_iff]