mapsTo_Ioi

Mathlib.Order.Interval.Set.Image

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

English

If f is strictly increasing, then f maps the ray Ioi a into Ioi (f(a)).

Русский

Если f строго возрастает, то образ луча Ioi a принадлежит Ioi(f(a)).

LaTeX

$$$StrictMono(f) \Rightarrow \forall x:\alpha,\ x > a \Rightarrow f(x) > f(a)$$$

Lean4

theorem mapsTo_Ioi (h : StrictMono f) : MapsTo f (Ioi a) (Ioi (f a)) :=
  (h.strictMonoOn _).mapsTo_Ioi

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

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

Разделы

Аффилиация

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