ofLowerSetOrderIso

Mathlib.Topology.Order.UpperLowerSetTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithLowerSet.ofLowerSetOrderIso

English

There is an order isomorphism between WithLowerSet α and α given by a ↦ ofLowerSet(a).

Русский

Существует упорядоченное изоморфизм между WithLowerSet α и α, задаваемый a ↦ ofLowerSet(a).

LaTeX

$$$ \mathrm{WithLowerSet}(\alpha) \cong_o \alpha.$$$

Lean4

/-- `ofLowerSet` as an `OrderIso` -/
def ofLowerSetOrderIso : WithLowerSet α ≃o α where
  toEquiv := ofLowerSet
  map_rel_iff' := ofLowerSet_le_iff

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

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

Разделы

Аффилиация

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