exists_series_of_coheight_eq_coe — Mathlib

English

If coheight a = n (cast), then there exists p : LTSeries α with head p.head = a and p.length = n.

Русский

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

LaTeX

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

Lean4

theorem exists_series_of_coheight_eq_coe (a : α) {n : ℕ} (h : coheight a = n) :
    ∃ p : LTSeries α, p.head = a ∧ p.length = n :=
  exists_series_of_le_coheight a (le_of_eq h.symm)

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