image_Iio

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#InitialSeg.image_Iio

English

For a, the image of the open interval Iio(a) under f equals Iio(f(a)).

Русский

Образ открытого отрезка Iio(a) под действием f совпадает с Iio(f(a)).

LaTeX

$$f'' Iio(a) = Iio(f(a))$$

Lean4

theorem image_Iio [PartialOrder α] (f : α ≤i β) (a : α) : f '' Set.Iio a = Set.Iio (f a) :=
  f.toOrderEmbedding.image_Iio f.isLowerSet_range a

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

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

Разделы

Аффилиация

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