exists_series_of_le_coheight — Mathlib

English

If n ≤ coheight a, there exists p : LTSeries α with head p.head = a and p.length = n.

Русский

Если n ≤ coheight a, существует p : LTSeries α с head = a и length = n.

LaTeX

$$$ n \le \operatorname{coheight}(a) \Rightarrow \exists p:\ LTSeries\alpha,\ p.head = a ∧ p.length = n $$$

Lean4

theorem exists_series_of_le_coheight (a : α) {n : ℕ} (h : n ≤ coheight a) :
    ∃ p : LTSeries α, p.head = a ∧ p.length = n :=
  by
  obtain ⟨p, hp, hl⟩ := exists_series_of_le_height (α := αᵒᵈ) a h
  exact ⟨p.reverse, by simpa, by simpa⟩

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