mapsTo_Ioo

Mathlib.Order.Interval.Set.Image

URI: https://scilib.ai/kg/mathlib#StrictMono.mapsTo_Ioo

English

If f is strictly increasing, then f maps the open interval Ioo a b into Ioo (f(a)) (f(b)).

Русский

Если f строго возрастает, то образ открытого интервала Ioo a b лежит в Ioo(f(a)) (f(b)).

LaTeX

$$$StrictMono(f) \Rightarrow \forall x, a < x < b \Rightarrow f(a) < f(x) < f(b)$$$

Lean4

theorem mapsTo_Ioo (h : StrictMono f) : MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
  (h.strictMonoOn _).mapsTo_Ioo

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

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

Разделы

Аффилиация

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