coheight_le_coheight_apply_of_strictMono

English

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

Русский

Для строго монотонной функции f: coheight(x) ≤ coheight(f(x)) для всех x.

LaTeX

$$$ coheight(x) \le coheight(f(x)) $$$

Lean4

theorem coheight_le_coheight_apply_of_strictMono (f : α → β) (hf : StrictMono f) (x : α) :
    coheight x ≤ coheight (f x) :=
  by
  apply height_le_height_apply_of_strictMono (α := αᵒᵈ)
  exact fun _ _ h ↦ hf h

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