mapsTo_uIcc — Mathlib

English

If f is monotone on uIcc(a,b), then f maps uIcc(a,b) into uIcc(f(a), f(b)).

Русский

Если f монотонна на uIcc(a,b), то отображение f приxодит uIcc(a,b) в uIcc(f(a), f(b)).

LaTeX

$$$ (hf : MonotoneOn\ \\ f\\ (uIcc\\ a\\ b)) \\Rightarrow MapsTo\\ f\\ (uIcc\\ a\\ b)\\ (uIcc\\ (f\\ a)\\ (f\\ b)) $$$

Lean4

theorem _root_.MonotoneOn.mapsTo_uIcc (hf : MonotoneOn f (uIcc a b)) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
  rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf] <;> apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

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