coheight_eq_top_iff — Mathlib

English

If f is an order isomorphism, then coheight(f(x)) = coheight(x) for all x.

Русский

Если f — изоморфизм порядка, то coheight(f(x)) = coheight(x).

LaTeX

$$$ coheight(f(x)) = coheight(x) $$$

Lean4

/-- The coheight of an element is infinite iff there exist series of arbitrary length ending in that
element.
-/
theorem coheight_eq_top_iff {x : α} : coheight x = ⊤ ↔ ∀ n, ∃ p : LTSeries α, p.head = x ∧ p.length = n :=
  by
  convert height_eq_top_iff (α := αᵒᵈ) (x := x) using 2 with n
  constructor <;> (intro ⟨p, hp, hl⟩; use p.reverse; constructor <;> simpa)

Похожие утверждения