English
For all a ∈ α and ENat n, height(a) ≤ n iff every LTSeries ending at a has length ≤ n.
Русский
Для каждого a ∈ α и n ∈ ENat верно: height(a) ≤ n тогда и только тогда, когда каждая LTSeries, заканчивающаяся в a, имеет длину ≤ n.
LaTeX
$$$\operatorname{height}(a) \le n \;\iff\; \forall p : LTSeries(\alpha),\; p.last \le a \rightarrow p.length \le n.$$$
Lean4
theorem height_le_iff {a : α} {n : ℕ∞} : height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, p.last ≤ a → p.length ≤ n := by
rw [height, iSup₂_le_iff]