map_refl

Mathlib.Order.UpperLower.CompleteLattice

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

English

The map induced by the identity isomorphism is the identity on UpperSet.

Русский

Отображение, порождаемое тождественным изоморфизмом, является тождественным на UpperSet.

LaTeX

$$$ \text{map}(\text{OrderIso.refl}(\alpha)) = \text{OrderIso.refl}(\text{UpperSet}(\alpha)) $$$

Lean4

@[simp]
theorem map_refl : map (OrderIso.refl α) = OrderIso.refl _ :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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