topToPreord — Mathlib

English

An Alexandrov-discrete space is isomorphic to the upper set topology of its specialization order.

Русский

Пространство Александрова-дискретности изоморфно верхнему множеству топологии специализации.

LaTeX

$$$\text{homeoWithUpperSetTopologyorderIso}(\alpha)$ is a Homeomorph between $\alpha$ and $\text{WithUpperSet}(\operatorname{Specialization}(\alpha))$.$$

Lean4

/-- Sends a topological space to its specialisation order. -/
@[simps]
def topToPreord : TopCat ⥤ Preord where
  obj X := .of <| Specialization X
  map f := Preord.ofHom <| Specialization.map f.hom

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