English
Embedding α into WithTop α preserves height: height(x) = height((withTop x)) under the appropriate injection.
Русский
Вставка α в WithTop α сохраняет высоту через соответствующее отображение: height(x) = height(WithTop x).
LaTeX
$$$$\\operatorname{height}(x) = \\operatorname{height}(x)\\;.$$$$
Lean4
@[simp]
theorem height_coe_withTop (x : α) : height (x : WithTop α) = height x :=
by
apply le_antisymm
· apply height_le
intro p hlast
let p' : LTSeries α :=
{ length := p.length
toFun := fun i =>
(p i).untop
(by
apply WithTop.lt_top_iff_ne_top.mp
apply lt_of_le_of_lt
· exact p.monotone (Fin.le_last _)
· rw [RelSeries.last] at hlast
simp [hlast])
step := fun i => by simpa [WithTop.untop_lt_iff, WithTop.coe_untop] using p.step i }
have hlast' : p'.last = x := by simp only [p', RelSeries.last, WithTop.untop_eq_iff, ← hlast]
suffices p'.length ≤ height p'.last by
rw [hlast'] at this
simpa [p'] using this
apply length_le_height_last
· apply height_le
intro p hlast
let p' := p.map _ WithTop.coe_strictMono
apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])
