mapsTo_Ioi

Mathlib.Order.Interval.Set.Image

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

English

If f is strictly anti-monotone, then f maps Ioi a into Iio (f(a)).

Русский

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

LaTeX

$$$StrictAnti(f) \Rightarrow \forall x, x \ge a \Rightarrow f(x) < f(a)$$$

Lean4

theorem mapsTo_Ioi (h : StrictAnti f) : MapsTo f (Ioi a) (Iio (f a)) :=
  (h.strictAntiOn _).mapsTo_Ioi

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

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

Разделы

Аффилиация

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