image_Icc_subset — Mathlib

English

Let f be monotone between preorder sets. Then the image of the closed interval [a, b] is contained in the closed interval [f(a), f(b)].

Русский

Пусть f монотонна между частично упорядоченными множествами. Образ отрезка [a, b] под f лежит в отрезке [f(a), f(b)].

LaTeX

$$$f(Icc(a,b)) \subseteq Icc(f(a), f(b))$$$

Lean4

theorem image_Icc_subset (h : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
  (h.monotoneOn _).image_Icc_subset

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