English
The coheight of a equals the supremum of lengths of LTSeries whose head is a.
Русский
Ко‑высота a равна супремуму длин LTSeries, у которых head равен a.
LaTeX
$$$\operatorname{coheight}(a) = \sup\{ \operatorname{length}(p) : p : LTSeries(\alpha), p.head = a \}. $$$
Lean4
/-- Alternative definition of coheight, with the supremum only ranging over those series
that begin at `a`.
-/
theorem coheight_eq_iSup_head_eq (a : α) : coheight a = ⨆ (p : LTSeries α) (_ : p.head = a), ↑(p.length) :=
by
change height (α := αᵒᵈ) a = ⨆ (p : LTSeries α) (_ : p.head = a), ↑(p.length)
rw [height_eq_iSup_last_eq]
apply
Equiv.iSup_congr
⟨RelSeries.reverse, RelSeries.reverse, fun _ ↦ RelSeries.reverse_reverse _, fun _ ↦ RelSeries.reverse_reverse _⟩
simp
