English
If f is an order isomorphism, then height(f(x)) = height(x) for all x.
Русский
Если f — допустимая изоморфия порядка, то высота x сохраняется: height(f(x)) = height(x).
LaTeX
$$$ height(f(x)) = height(x) $$$
Lean4
/-- The height of an element is infinite iff there exist series of arbitrary length ending in that
element.
-/
theorem height_eq_top_iff {x : α} : height x = ⊤ ↔ ∀ n, ∃ p : LTSeries α, p.last = x ∧ p.length = n
where
mp h
n := by
apply exists_series_of_le_height x (n := n)
simp [h]
mpr
h := by
rw [height_eq_iSup_last_eq, iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def]
push_neg
intro n
obtain ⟨p, hlast, hp⟩ := h (n + 1)
exact ⟨p.length, ⟨⟨⟨p, hlast⟩, by simp [hp]⟩, by simp [hp]⟩⟩
