map_Iic

Mathlib.Order.UpperLower.Principal

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

English

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

Русский

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

LaTeX

$$map f (Iic a) = Iic (f a)$$

Lean4

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

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

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

Разделы

Аффилиация

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