height_add_one_le — Mathlib

English

If a < b, then height a + 1 ≤ height b.

Русский

Если a < b, то height a + 1 ≤ height b.

LaTeX

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

Lean4

theorem height_add_one_le {a b : α} (hab : a < b) : height a + 1 ≤ height b := by
  cases hfin : height a with
  |
    top =>
    have : ⊤ ≤ height b := by
      rw [← hfin]
      gcongr
    simp [this]
  | coe n =>
    apply Order.add_one_le_of_lt
    rw [← hfin]
    gcongr
    simp [hfin]
      /- For elements of finite height, `coheight` is strictly antitone. -/

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