coheight_le_iff' — Mathlib

English

Variant expression for coheight using head-based supremum.

Русский

Вариант выражения ко‑высоты через супремум по серий с head = a.

LaTeX

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

Lean4

/-- Variant of `coheight_le_iff` ranging only over those series that begin exactly on `a`.
-/
theorem coheight_le_iff' {a : α} {n : ℕ∞} : coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, p.head = a → p.length ≤ n := by
  rw [coheight_eq_iSup_head_eq, iSup₂_le_iff]

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