image_monotone — Mathlib

English

If e is monotone on α, then the induced map on s → e[s] is monotone as a function from the subtype s to the image e[s].

Русский

Если e монотонна на α, то соответствующая отображение на s → e[s] является монотонной функцией от подпредмета s к образу e[s].

LaTeX

$$$ (\forall x,y\in s) \, x \le y \Rightarrow e(x) \le e(y) $$$

Lean4

theorem image_monotone (hs : Monotone e) : Monotone (e.image s) :=
  hs.comp (Subtype.mono_coe _)

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