image_Iic_subset

Mathlib.Order.Interval.Set.Image

URI: https://scilib.ai/kg/mathlib#MonotoneOn.image_Iic_subset

English

If f is monotone on Iic b, then the image of Iic b under f lies inside Iic(f b).

Русский

Если f монотонна на Iic b, то образ Iic b под действием f лежит внутри Iic(f b).

LaTeX

$$$MonotoneOn(f)\ (Iic b) \Rightarrow f '' Iic b \subseteq Iic (f b)$$$

Lean4

theorem image_Iic_subset (h : MonotoneOn f (Iic b)) : f '' Iic b ⊆ Iic (f b) :=
  h.mapsTo_Iic.image_subset

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

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

Разделы

Аффилиация

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