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
@[match_pattern]
toEquiv
is the "identity" function to the Specialization
of a type.
Equations
Instances For
@[match_pattern]
ofEquiv
is the identity function from the Specialization
of a type.
Equations
Instances For
@[simp]
@[simp]
def
Specialization.rec
{α : Type u_1}
{β : Specialization α → Sort u_4}
(h : (a : α) → β (toEquiv a))
(a : Specialization α)
:
β a
A recursor for Specialization
. Use as induction x
.
Instances For
Equations
Equations
@[simp]
theorem
Specialization.ofEquiv_specializes_ofEquiv
{α : Type u_1}
[TopologicalSpace α]
{a b : Specialization α}
:
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.
Equations
Instances For
@[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.
Equations
Instances For
An Alexandrov-discrete space is isomorphic to the upper set topology of its specialisation order.
Equations
Instances For
Sends a topological space to its specialisation order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]