height_le_height_apply_of_strictMono

English

For a strictly monotone function f, height(x) ≤ height(f(x)) for all x.

Русский

Пусть f — строго монотонная функция; тогда height(x) ≤ height(f(x)) для всех x.

LaTeX

$$$ height(x) \le height(f(x)) $$$

Lean4

theorem height_le_height_apply_of_strictMono (f : α → β) (hf : StrictMono f) (x : α) : height x ≤ height (f x) :=
  by
  simp only [height_eq_iSup_last_eq]
  apply iSup₂_le
  intro p hlast
  apply le_iSup₂_of_le (p.map f hf) (by simp [hlast]) (by simp)

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