English
For a ∈ α and n ∈ ℕ, if n ≤ height a, there exists p : LTSeries α with head p.head = a and p.length = n.
Русский
Для элемента a ∈ α и натурального n, если n ≤ height a, существует p : LTSeries α с head = a и length = n.
LaTeX
$$$ (a) \ (n) \ (n \le height(a)) \Rightarrow \exists p:\ LTSeries\alpha,\ p.head = a ∧ p.length = n $$$
Lean4
/-- Another characterization of height, based on the supremum of the heights of elements below. -/
theorem height_eq_iSup_lt_height (x : α) : height x = ⨆ y < x, height y + 1 :=
by
apply le_antisymm
· apply height_le
intro p hp
cases hlen : p.length with
| zero => simp
| succ n =>
apply le_iSup_of_le p.eraseLast.last
apply le_iSup_of_le (by rw [← hp]; exact p.eraseLast_last_rel_last (by cutsat))
rw [height_add_const]
apply le_iSup₂_of_le p.eraseLast (by rfl) (by simp [hlen])
· apply iSup₂_le; intro y hyx
rw [height_add_const]
apply iSup₂_le; intro p hp
apply le_iSup₂_of_le (p.snoc x (hp ▸ hyx)) (by simp) (by simp)
