Inseparable points in a topological space #
In this file we define
-
specializes
(notation:x ⤳ y
) : a relation saying that𝓝 x ≤ 𝓝 y
; -
inseparable
: a relation saying that two points in a topological space have the same neighbourhoods; equivalently, they can't be separated by an open set; -
inseparable_setoid X
: same relation, as asetoid
; -
separation_quotient X
: the quotient ofX
by itsinseparable_setoid
.
We also prove various basic properties of the relation inseparable
.
Notations #
x ⤳ y
: notation forspecializes x y
;x ~ y
is used as a local notation forinseparable x y
;𝓝 x
is the neighbourhoods filternhds x
of a pointx
, defined elsewhere.
Tags #
topological space, separation setoid
specializes
relation #
x
specializes to y
(notation: x ⤳ y
) if either of the following equivalent properties
hold:
𝓝 x ≤ 𝓝 y
; this property is used as the definition;pure x ≤ 𝓝 y
; in other words, any neighbourhood ofy
containsx
;y ∈ closure {x}
;closure {y} ⊆ closure {x}
;- for any closed set
s
we havex ∈ s → y ∈ s
; - for any open set
s
we havey ∈ s → x ∈ s
; y
is a cluster point of the filterpure x = 𝓟 {x}
.
This relation defines a preorder
on X
. If X
is a T₀ space, then this preorder is a partial
order. If X
is a T₁ space, then this partial order is trivial : x ⤳ y ↔ x = y
.
A collection of equivalent definitions of x ⤳ y
. The public API is given by iff
lemmas
below.
Alias of the forward direction of specializes_iff_nhds
.
Alias of the forward direction of specializes_iff_pure
.
Alias of the forward direction of specializes_iff_mem_closure
.
Alias of the forward direction of specializes_iff_closure_subset
.
Specialization forms a preorder on the topological space.
A continuous function is monotone with respect to the specialization preorders on the domain and the codomain.
inseparable
relation #
Two points x
and y
in a topological space are inseparable
if any of the following
equivalent properties hold:
𝓝 x = 𝓝 y
; we use this property as the definition;- for any open set
s
,x ∈ s ↔ y ∈ s
, seeinseparable_iff_open
; - for any closed set
s
,x ∈ s ↔ y ∈ s
, seeinseparable_iff_closed
; x ∈ closure {y}
andy ∈ closure {x}
, seeinseparable_iff_mem_closure
;closure {x} = closure {y}
, seeinseparable_iff_closure_eq
.
Equations
- inseparable x y = (nhds x = nhds y)
Separation quotient #
In this section we define the quotient of a topological space by the inseparable
relation.
A setoid
version of inseparable
, used to define the separation_quotient
.
Equations
- inseparable_setoid X = {r := inseparable _inst_1, iseqv := _}
The quotient of a topological space by its inseparable_setoid
. This quotient is guaranteed to
be a T₀ space.
Equations
The natural map from a topological space to its separation quotient.