A T₀ space, also known as a Kolmogorov space, is a topological space
where for every pair x ≠ y
, there is an open set containing one but not the other.
Instances
- t1 : ∀ (x : α), is_closed {x}
A T₁ space, also known as a Fréchet space, is a topological space
where every singleton set is closed. Equivalently, for every pair
x ≠ y
, there is an open set containing x
and not y
.
A point x
in a discrete subset s
of a topological space admits a neighbourhood
that only meets s
at x
.
For point x
in a discrete subset s
of a topological space, there is a set U
such that
U
is a punctured neighborhood ofx
(ie.U ∪ {x}
is a neighbourhood ofx
),U
is disjoint froms
.
Let X
be a topological space and let s, t ⊆ X
be two subsets. If there is an inclusion
t ⊆ s
, then the topological space structure on t
induced by X
is the same as the one
obtained by the induced topological space structure on s
.
This lemma characterizes discrete topological spaces as those whose singletons are neighbourhoods.
The topology pulled-back under an inclusion f : X → Y
from the discrete topology (⊥
) is the
discrete topology.
This version does not assume the choice of a topology on either the source X
nor the target Y
of the inclusion f
.
The topology induced under an inclusion f : X → Y
from the discrete topological space Y
is the discrete topology on X
.
Let s, t ⊆ X
be two subsets of a topological space X
. If t ⊆ s
and the topology induced
by X
on s
is discrete, then also the topology induces on t
is discrete.
A T₂ space, also known as a Hausdorff space, is one in which for every
x ≠ y
there exists disjoint open sets around x
and y
. This is
the most widely used of the separation axioms.
Properties of Lim
and lim
#
In this section we use explicit nonempty α
instances for Lim
and lim
. This way the lemmas
are useful without a nonempty α
instance.
Instances of t2_space
typeclass #
We use two lemmas to prove that various standard constructions generate Hausdorff spaces from Hausdorff spaces:
-
separated_by_continuous
says that two pointsx y : α
can be separated by open neighborhoods provided that there exists a continuous mapf
: α → βwith a Hausdorff codomain such that
f x ≠ f y. We use this lemma to prove that topological spaces defined using
induced` are Hausdorff spaces. -
separated_by_open_embedding
says that for an open embeddingf : α → β
of a Hausdorff spaceα
, the images of two distinct pointsx y : α
,x ≠ y
can be separated by open neighborhoods. We use this lemma to prove that topological spaces defined usingcoinduced
are Hausdorff spaces.
If two continuous maps are equal on s
, then they are equal on the closure of s
.
If two continuous functions are equal on a dense set, then they are equal.
In a t2_space
, every compact set is closed.
If a compact set is covered by two open sets, then we can cover it by two compact subsets.
For every finite open cover Uᵢ
of a compact set, there exists a compact cover Kᵢ ⊆ Uᵢ
.
In a locally compact T₂ space, every point has an open neighborhood with compact closure
- to_t1_space : t1_space α
- regular : ∀ {s : set α} {a : α}, is_closed s → a ∉ s → (∃ (t : set α), is_open t ∧ s ⊆ t ∧ 𝓝[t] a = ⊥)
A T₃ space, also known as a regular space (although this condition sometimes
omits T₂), is one in which for every closed C
and x ∉ C
, there exist
disjoint open sets containing x
and C
respectively.
- to_t1_space : t1_space α
- normal : ∀ (s t : set α), is_closed s → is_closed t → disjoint s t → (∃ (u v : set α), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ disjoint u v)
A T₄ space, also known as a normal space (although this condition sometimes
omits T₂), is one in which for every pair of disjoint closed sets C
and D
,
there exist disjoint open sets containing C
and D
respectively.
Instances
In a compact t2 space, the connected component of a point equals the intersection of all its clopen neighbourhoods.
connected_components α
is Hausdorff when α
is Hausdorff and compact