height_nat — Mathlib

English

In a NoMaxOrder, every coheight is top.

Русский

В NoMaxOrder для каждого элемента ко-высота равна верхней границе.

LaTeX

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

Lean4

@[simp]
theorem height_nat (n : ℕ) : height n = n := by
  induction n using Nat.strongRecOn with
  | ind n ih =>
    apply le_antisymm
    · apply height_le_coe_iff.mpr
      simp +contextual only [ih, Nat.cast_lt, implies_true]
    · exact length_le_height_last (p := LTSeries.range n)

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