coheight_le_iff — Mathlib

English

If every LTSeries with head a has length ≤ n, then coheight(a) ≤ n.

Русский

Если для каждого LTSeries с head = a выполнено p.length ≤ n, тогда coheight(a) ≤ n.

LaTeX

$$$\bigl(\forall p : LTSeries(\alpha), p.head = a \rightarrow p.length \le n\bigr) \Rightarrow \operatorname{coheight}(a) \le n.$$$

Lean4

theorem coheight_le_iff {a : α} {n : ℕ∞} : coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, a ≤ p.head → p.length ≤ n := by
  rw [coheight_eq, iSup₂_le_iff]

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