map_Iio

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#LowerSet.map_Iio

English

Under an order isomorphism f, the image of Iio under map f is Iio of the image: map f(Iio a) = Iio(f(a)).

Русский

При изоморфизме порядка f образ Iio совпадает с Iio образа: map f(Iio a) = Iio(f(a)).

LaTeX

$$map f (Iio a) = Iio (f a)$$

Lean4

@[simp]
theorem map_Iio (f : α ≃o β) (a : α) : map f (Iio a) = Iio (f a) :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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