Specialization order #
This file defines a type synonym for a topological space considered with its specialisation order.
Type synonym for a topological space considered with its specialisation order.
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 α)
:
↑Specialization.toEquiv (↑Specialization.ofEquiv a) = a
@[simp]
theorem
Specialization.ofEquiv_toEquiv
{α : Type u_1}
(a : α)
:
↑Specialization.ofEquiv (↑Specialization.toEquiv a) = a
@[simp]
def
Specialization.rec
{α : Type u_1}
{β : Specialization α → Sort u_4}
(h : (a : α) → β (↑Specialization.toEquiv a))
(a : α)
:
β a
A recursor for Specialization
. Use as induction x using Specialization.rec
.
Instances For
@[simp]
@[simp]
theorem
Specialization.ofEquiv_specializes_ofEquiv
{α : Type u_1}
[TopologicalSpace α]
{a : Specialization α}
{b : Specialization α}
:
@[simp]
theorem
Specialization.isOpen_toEquiv_preimage
{α : Type u_1}
[TopologicalSpace α]
[AlexandrovDiscrete α]
{s : Set (Specialization α)}
:
IsOpen (↑Specialization.toEquiv ⁻¹' s) ↔ IsUpperSet s
@[simp]
theorem
Specialization.isUpperSet_ofEquiv_preimage
{α : Type u_1}
[TopologicalSpace α]
[AlexandrovDiscrete α]
{s : Set α}
:
IsUpperSet (↑Specialization.ofEquiv ⁻¹' s) ↔ IsOpen s
def
Specialization.map
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(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}
[TopologicalSpace α]
:
Specialization.map (ContinuousMap.id α) = OrderHom.id
@[simp]
theorem
Specialization.map_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
(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]
@[simp]
Sends a topological space to its specialisation order.