coheight_add_one_le — Mathlib

English

If b < a, then coheight(a) + 1 ≤ coheight(b).

Русский

Если b < a, то coheight(a) + 1 ≤ coheight(b).

LaTeX

$$$ b < a \Rightarrow \operatorname{coheight}(a) + 1 \le \operatorname{coheight}(b) $$$

Lean4

theorem coheight_add_one_le {a b : α} (hab : b < a) : coheight a + 1 ≤ coheight b := by
  cases hfin : coheight a with
  |
    top =>
    have : ⊤ ≤ coheight b := by
      rw [← hfin]
      gcongr
    simp [this]
  | coe n =>
    apply Order.add_one_le_of_lt
    rw [← hfin]
    gcongr
    simp [hfin]

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