height_le_iff' — Mathlib

English

Height a equals the supremum of lengths of LTSeries ending at a.

Русский

Высота a равна супремуму длин LTSeries, оканчивающихся в a.

LaTeX

$$$\operatorname{height}(a) = \sup\{ \operatorname{length}(p) : p : LTSeries(\alpha), p.last = a \}. $$$

Lean4

/-- Variant of `height_le_iff` ranging only over those series that end exactly on `a`.
-/
theorem height_le_iff' {a : α} {n : ℕ∞} : height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, p.last = a → p.length ≤ n :=
  by
  constructor
  · rw [height_le_iff]
    exact fun h p hlast => h (le_of_eq hlast)
  · exact height_le

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