image_Ici_subset

Mathlib.Order.Interval.Set.Image

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

English

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

Русский

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

LaTeX

$$$MonotoneOn(f)\ (Ici\ a) \Rightarrow f '' Ici a \subseteq Ici (f a)$$$

Lean4

theorem image_Ici_subset (h : MonotoneOn f (Ici a)) : f '' Ici a ⊆ Ici (f a) :=
  h.mapsTo_Ici.image_subset

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

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

Разделы

Аффилиация

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