English
The coheight function is antitone with respect to the underlying order.
Русский
Функция ко‑высоты антиинормальна по отношению к исходному порядку: если a ≤ b, то coheight(a) ≥ coheight(b).
LaTeX
$$$\forall a,b:\alpha,\ a \le b \Rightarrow \operatorname{coheight}(a) \ge \operatorname{coheight}(b).$$$
Lean4
theorem length_le_height {p : LTSeries α} {x : α} (hlast : p.last ≤ x) : p.length ≤ height x :=
by
by_cases hlen0 : p.length ≠ 0
· let p' :=
p.eraseLast.snoc x
(by
apply lt_of_lt_of_le
· apply p.step ⟨p.length - 1, by cutsat⟩
· convert hlast
simp only [Fin.succ_mk, RelSeries.last, Fin.last]
congr; cutsat)
suffices p'.length ≤ height x by
simp [p'] at this
convert this
norm_cast
cutsat
refine le_iSup₂_of_le p' ?_ le_rfl
simp [p']
· simp_all
