height_strictMono — Mathlib

English

If x < y and height x is finite (height x < ⊤), then height x < height y.

Русский

Если x < y и height x < ⊤, то height x < height y.

LaTeX

$$$ (x < y) \land (\operatorname{height}(x) < \top) \Rightarrow \operatorname{height}(x) < \operatorname{height}(y) $$$

Lean4

@[gcongr]
theorem height_strictMono {x y : α} (hxy : x < y) (hfin : height x < ⊤) : height x < height y :=
  by
  rw [← ENat.add_one_le_iff hfin.ne, height_add_const, iSup₂_le_iff]
  intro p hlast
  have := length_le_height_last (p := p.snoc y (by simp [*]))
  simpa using this

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