mapsTo_Iic

Mathlib.Order.Interval.Set.Image

URI: https://scilib.ai/kg/mathlib#Monotone.mapsTo_Iic

English

Let f be monotone. Then for every b ∈ α and every x ≤ b, we have f(x) ≤ f(b).

Русский

Пусть f монотонна. Тогда для любого b ∈ α и любого x ≤ b выполняется f(x) ≤ f(b).

LaTeX

$$$Monotone(f) \Rightarrow \forall x,b:\alpha,\ x \le b \Rightarrow f(x) \le f(b)$$$

Lean4

theorem mapsTo_Iic (h : Monotone f) : MapsTo f (Iic b) (Iic (f b)) :=
  (h.monotoneOn _).mapsTo_Iic

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

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

Разделы

Аффилиация

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