mapsTo_Iio

Mathlib.Order.Interval.Set.Image

URI: https://scilib.ai/kg/mathlib#StrictAntiOn.mapsTo_Iio

English

If f is strictly antitone on Iic b, then for all x < b we have f(x) > f(b).

Русский

Если f строго антимонотонна на Iic b, то для всех x < b выполняется f(x) > f(b).

LaTeX

$$$$ \\forall b\\; (\\text{StrictAntiOn } f\\ (\\Iic b))\\;:\\; \\mathrm{MapsTo}\\, f\\,(\\Iio b)\\,(\\Ioi (f b)). $$$$

Lean4

theorem mapsTo_Iio (h : StrictAntiOn f (Iic b)) : MapsTo f (Iio b) (Ioi (f b)) := fun _c hc ↦ h hc.le le_rfl hc

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

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

Разделы

Аффилиация

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