mapsTo_Ioc

Mathlib.Order.Interval.Set.Image

URI: https://scilib.ai/kg/mathlib#StrictAnti.mapsTo_Ioc

English

If f is strictly antitone, then f maps the open-closed interval Ioc a b into Ico (f(b)) (f(a)).

Русский

Если f строго антимонотонна, образ Ioc a b лежит в Ico(f(b), f(a)).

LaTeX

$$$f(Ioc(a,b)) \subseteq Ico(f(b), f(a))$$$

Lean4

theorem mapsTo_Ioc (h : StrictAnti f) : MapsTo f (Ioc a b) (Ico (f b) (f a)) :=
  (h.strictAntiOn _).mapsTo_Ioc

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

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

Разделы

Аффилиация

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