height_eq_iSup_last_eq — Mathlib

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]

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