coheight_of_noMaxOrder — Mathlib

English

In a NoMinOrder, every height is top.

Русский

В NoMinOrder каждая высота равна топу.

LaTeX

$$$\forall a,\ \operatorname{height}(a) = \top$$$

Lean4

@[simp]
theorem coheight_of_noMaxOrder [NoMaxOrder α] (a : α) : coheight a = ⊤ :=
  by
  obtain ⟨f, hstrictmono⟩ := Nat.exists_strictMono ↑(Set.Ioi a)
  apply coheight_eq_top_iff.mpr
  intro m
  use { length := m, toFun := fun i => if i = 0 then a else f i, step := ?step }
  case h => simp [RelSeries.head]
  case step =>
    intro ⟨i, hi⟩
    by_cases hzero : i = 0
    · subst i
      exact (f 1).prop
    · suffices f i < f (i + 1) by simp [Fin.ext_iff, hzero, this]
      apply hstrictmono
      cutsat

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