mapsTo_Icc

Mathlib.Order.Interval.Set.Image

URI: https://scilib.ai/kg/mathlib#Antitone.mapsTo_Icc

English

If f is antitone, then f maps the interval [a,b] into [f(b), f(a)].

Русский

Если f антимонтонична, то отображение [a,b] лежит в [f(b), f(a)].

LaTeX

$$$Antitone(f) \Rightarrow \forall x, a \le x \le b \Rightarrow f(b) \le f(x) \le f(a)$$$

Lean4

theorem mapsTo_Icc (h : Antitone f) : MapsTo f (Icc a b) (Icc (f b) (f a)) :=
  (h.antitoneOn _).mapsTo_Icc

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

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

Разделы

Аффилиация

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