mapsTo_Ici

Mathlib.Order.Interval.Set.Image

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

English

If f is antitone on Ici a, then for all x ≥ a we have f(x) ≤ f(a).

Русский

Если f антимонотонна на Ici a, то для всех x ≥ a выполняется f(x) ≤ f(a).

LaTeX

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

Lean4

theorem mapsTo_Ici (h : AntitoneOn f (Ici a)) : MapsTo f (Ici a) (Iic (f a)) := fun _ _ ↦ by aesop

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

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

Разделы

Аффилиация

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