image_Ioc_subset

Mathlib.Order.Interval.Set.Image

URI: https://scilib.ai/kg/mathlib#StrictMono.image_Ioc_subset

English

If f is strictly monotone, then f maps Ioc a b into Ioc (f a) (f b).

Русский

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

LaTeX

$$$f(Ioc(a,b)) \subseteq Ioc(f(a), f(b))$$$

Lean4

theorem image_Ioc_subset (h : StrictMono f) : f '' Ioc a b ⊆ Ioc (f a) (f b) :=
  (h.strictMonoOn _).image_Ioc_subset

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

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

Разделы

Аффилиация

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