height_le_iff — Mathlib

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]

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