coheight_le — Mathlib

English

A basic property of coheight: if every LTSeries with head a has a bounded length ≤ n, then coheight a ≤ n.

Русский

Базовое свойство ко‑высоты: если каждая LTSeries с head = a имеет длину ≤ n, то ко‑высота a ≤ n.

LaTeX

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

Lean4

theorem coheight_le {a : α} {n : ℕ∞} (h : ∀ (p : LTSeries α), p.head = a → p.length ≤ n) : coheight a ≤ n :=
  coheight_le_iff'.mpr h

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