orderIsoSpecializationWithUpperSetTopology

English

A preorder is isomorphic to the specialization order of its upper set topology.

Русский

Любой предорядок изоморфен порядку специализации верхнего множестваTopology.

LaTeX

$$def orderIsoSpecializationWithUpperSetTopology (α : Type*) [Preorder α] : α ≃o Specialization (WithUpperSet α)$$

Lean4

/-- A preorder is isomorphic to the specialisation order of its upper set topology. -/
def orderIsoSpecializationWithUpperSetTopology (α : Type*) [Preorder α] : α ≃o Specialization (WithUpperSet α)
    where
  toEquiv := toUpperSet.trans toEquiv
  map_rel_iff' := by simp

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