mapsTo_Ici

Mathlib.Order.Interval.Set.Image

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

English

If f is monotone, then for all a, f maps [a, ∞) into [f(a), ∞).

Русский

Если f монотонна, то для любого a отображение [a, ∞) лежит в [f(a), ∞).

LaTeX

$$$$ \\forall a\\; (\\text{Monotone } f)\\;:\\; \\mathrm{MapsTo}\\, f\\,(\\Ici a)\\,(\\Ici (f a)). $$$$

Lean4

theorem mapsTo_Ici (h : Monotone f) : MapsTo f (Ici a) (Ici (f a)) :=
  (h.monotoneOn _).mapsTo_Ici

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

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

Разделы

Аффилиация

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