map_Ioi

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#UpperSet.map_Ioi

English

For any order isomorphism f, the image of Ioi a under map f is Ioi(f a).

Русский

Образ Ioi(a) под отображением f есть Ioi(f(a)).

LaTeX

$$$ \mathrm{map} \, f \, (\mathrm{Ioi}(a)) = \mathrm{Ioi}(f(a)) $$$

Lean4

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

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

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

Разделы

Аффилиация

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