# Documentation

Mathlib.Topology.Specialization

# Specialization order #

This file defines a type synonym for a topological space considered with its specialisation order.

def Specialization (α : Type u_1) :
Type u_1

Type synonym for a topological space considered with its specialisation order.

Instances For
@[match_pattern]
def Specialization.toEquiv {α : Type u_1} :

toEquiv is the "identity" function to the Specialization of a type.

Instances For
@[match_pattern]
def Specialization.ofEquiv {α : Type u_1} :

ofEquiv is the identity function from the Specialization of a type.

Instances For
@[simp]
theorem Specialization.toEquiv_symm {α : Type u_1} :
Specialization.toEquiv.symm = Specialization.ofEquiv
@[simp]
theorem Specialization.ofEquiv_symm {α : Type u_1} :
Specialization.ofEquiv.symm = Specialization.toEquiv
@[simp]
theorem Specialization.toEquiv_ofEquiv {α : Type u_1} (a : ) :
Specialization.toEquiv (Specialization.ofEquiv a) = a
@[simp]
theorem Specialization.ofEquiv_toEquiv {α : Type u_1} (a : α) :
Specialization.ofEquiv (Specialization.toEquiv a) = a
@[simp]
theorem Specialization.toEquiv_inj {α : Type u_1} {a : α} {b : α} :
Specialization.toEquiv a = Specialization.toEquiv b a = b
@[simp]
theorem Specialization.ofEquiv_inj {α : Type u_1} {a : } {b : } :
Specialization.ofEquiv a = Specialization.ofEquiv b a = b
def Specialization.rec {α : Type u_1} {β : Sort u_4} (h : (a : α) → β (Specialization.toEquiv a)) (a : α) :
β a

A recursor for Specialization. Use as induction x using Specialization.rec.

Instances For
instance Specialization.instPreorder {α : Type u_1} [] :
instance Specialization.instPartialOrder {α : Type u_1} [] [] :
@[simp]
theorem Specialization.toEquiv_le_toEquiv {α : Type u_1} [] {a : α} {b : α} :
Specialization.toEquiv a Specialization.toEquiv b b a
@[simp]
theorem Specialization.ofEquiv_specializes_ofEquiv {α : Type u_1} [] {a : } {b : } :
Specialization.ofEquiv a Specialization.ofEquiv b b a
@[simp]
theorem Specialization.isOpen_toEquiv_preimage {α : Type u_1} [] {s : } :
IsOpen (Specialization.toEquiv ⁻¹' s)
@[simp]
theorem Specialization.isUpperSet_ofEquiv_preimage {α : Type u_1} [] {s : Set α} :
IsUpperSet (Specialization.ofEquiv ⁻¹' s)
def Specialization.map {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :

A continuous map between topological spaces induces a monotone map between their specialization orders.

Instances For
@[simp]
theorem Specialization.map_id {α : Type u_1} [] :
= OrderHom.id
@[simp]
theorem Specialization.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : C(β, γ)) (f : C(α, β)) :

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

Instances For

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

Instances For
@[simp]
theorem topToPreord_map :
∀ {X Y : TopCat} (f : C(X, Y)), topToPreord.map f =
@[simp]
theorem topToPreord_obj (X : TopCat) :
topToPreord.obj X =

Sends a topological space to its specialisation order.

Instances For