mapsTo_uIcc

Mathlib.Order.Interval.Set.UnorderedInterval

URI: https://scilib.ai/kg/mathlib#Monotone.mapsTo_uIcc

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.Monotone.mapsTo_uIcc (hf : Monotone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
  (hf.monotoneOn _).mapsTo_uIcc

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru