exists_series_of_height_eq_coe — Mathlib

English

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

Русский

Если height a = n, то существует p : LTSeries α с last p.last = a и p.length = n.

LaTeX

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

Lean4

/-- For an element of finite height there exists a series ending in that element of that height. -/
theorem exists_series_of_height_eq_coe (a : α) {n : ℕ} (h : height a = n) :
    ∃ p : LTSeries α, p.last = a ∧ p.length = n :=
  exists_series_of_le_height a (le_of_eq h.symm)

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