Separation properties of topological spaces. #
This file defines the predicate separated
, and common separation axioms
(under the Kolmogorov classification).
Main definitions #
separated
: Twoset
s are separated if they are contained in disjoint open sets.t0_space
: A T₀/Kolmogorov space is a space where, for every two pointsx ≠ y
, there is an open set that contains one, but not the other.t1_space
: A T₁/Fréchet space is a space where every singleton set is closed. This is equivalent to, for every pairx ≠ y
, there existing an open set containingx
but noty
(t1_space_iff_exists_open
shows that these conditions are equivalent.)t2_space
: A T₂/Hausdorff space is a space where, for every two pointsx ≠ y
, there is two disjoint open sets, one containingx
, and the othery
.t2_5_space
: A T₂.₅/Urysohn space is a space where, for every two pointsx ≠ y
, there is two open sets, one containingx
, and the othery
, whose closures are disjoint.t3_space
: A T₃ space, is one where given any closedC
andx ∉ C
, there is disjoint open sets containingx
andC
respectively. Inmathlib
, T₃ implies T₂.₅.normal_space
: A T₄ space (sometimes referred to as normal, but authors vary on whether this includes T₂;mathlib
does), is one where given two disjoint closed sets, we can find two open sets that separate them. Inmathlib
, T₄ implies T₃.
Main results #
T₀ spaces #
is_closed.exists_closed_singleton
Given a closed setS
in a compact T₀ space, there is somex ∈ S
such that{x}
is closed.exists_open_singleton_of_open_finset
Given an openfinset
S
in a T₀ space, there is somex ∈ S
such that{x}
is open.
T₁ spaces #
is_closed_map_const
: The constant map is a closed map.discrete_of_t1_of_finite
: A finite T₁ space must have the discrete topology.
T₂ spaces #
t2_iff_nhds
: A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter.t2_iff_is_closed_diagonal
: A space is T₂ iff thediagonal
ofα
(that is, the set of all points of the form(a, a) : α × α
) is closed under the product topology.finset_disjoint_finset_opens_of_t2
: Any two disjoint finsets areseparated
.- Most topological constructions preserve Hausdorffness;
these results are part of the typeclass inference system (e.g.
embedding.t2_space
) set.eq_on.closure
: If two functions are equal on some sets
, they are equal on its closure.is_compact.is_closed
: All compact sets are closed.locally_compact_of_compact_nhds
: If every point has a compact neighbourhood, then the space is locally compact.tot_sep_of_zero_dim
: Ifα
has a clopen basis, it is atotally_separated_space
.loc_compact_t2_tot_disc_iff_tot_sep
: A locally compact T₂ space is totally disconnected iff it is totally separated.
If the space is also compact:
normal_of_compact_t2
: A compact T₂ space is anormal_space
.connected_components_eq_Inter_clopen
: The connected component of a point is the intersection of all its clopen neighbourhoods.compact_t2_tot_disc_iff_tot_sep
: Being atotally_disconnected_space
is equivalent to being atotally_separated_space
.connected_components.t2
:connected_components α
is T₂ forα
T₂ and compact.
T₃ spaces #
disjoint_nested_nhds
: Given two pointsx ≠ y
, we can find neighbourhoodsx ∈ V₁ ⊆ U₁
andy ∈ V₂ ⊆ U₂
, with theVₖ
closed and theUₖ
open, such that theUₖ
are disjoint.
Discrete spaces #
discrete_topology_iff_nhds
: Discrete topological spaces are those whose neighbourhood filters are thepure
filter (which is the principal filter at a singleton).induced_bot
/discrete_topology_induced
: The pullback of the discrete topology under an inclusion is the discrete topology.
References #
- t0 : ∀ ⦃x y : α⦄, inseparable x y → x = y
A T₀ space, also known as a Kolmogorov space, is a topological space such that for every pair
x ≠ y
, there is an open set containing one but not the other. We formulate the definition in terms
of the inseparable
relation.
Specialization forms a partial order on a t0 topological space.
Equations
- specialization_order α = {le := preorder.le (specialization_preorder α), lt := preorder.lt (specialization_preorder α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Given a closed set S
in a compact T₀ space,
there is some x ∈ S
such that {x}
is closed.
Given an open finite set S
in a T₀ space, there is some x ∈ S
such that {x}
is open.
- 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
.
In a t1_space
, relatively compact sets form a bornology. Its cobounded filter is
filter.coclosed_compact
. See also bornology.in_compact
the bornology of sets contained
in a compact set.
Equations
- bornology.relatively_compact α = {cobounded := filter.coclosed_compact α _inst_1, le_cofinite := _}
Removing a non-isolated point from a dense set, one still obtains a dense set.
Removing a finset from a dense set in a space without isolated points, one still obtains a dense set.
Removing a finite set from a dense set in a space without isolated points, one still obtains a dense set.
If a function to a t1_space
tends to some limit b
at some point a
, then necessarily
b = f a
.
To prove a function to a t1_space
is continuous at some point a
, it suffices to prove that
f
admits some limit at a
.
If the punctured neighborhoods of a point form a nontrivial filter, then any neighborhood is infinite.
The neighbourhoods filter of x
within s
, under the discrete topology, is equal to
the pure x
filter (which is the principal filter at the singleton {x}
.)
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.
Instances of this typeclass
- order_closed_topology.to_t2_space
- t2_5_space.t2_space
- discrete_topology.to_t2_space
- t3_space.t2_space
- t2_space_of_properly_discontinuous_smul_of_t2_space
- t2_space_of_properly_discontinuous_vadd_of_t2_space
- topological_space.t2_space_of_metrizable_space
- polish_space.t2_space
- priestley_space.to_t2_space
- subtype.t2_space
- prod.t2_space
- sum.t2_space
- Pi.t2_space
- sigma.t2_space
- connected_components.t2
- mul_opposite.t2_space
- add_opposite.t2_space
- continuous_map.t2_space
- ennreal.t2_space
- matrix.t2_space
- ereal.t2_space
- ultrafilter.t2_space
- stone_cech.t2_space
- CompHaus.t2_space
- continuous_monoid_hom.t2_space
- pontryagin_dual.t2_space
- Compactum.t2_space
A finite set can be separated by open sets.
A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter.
- t2_5 : ∀ (x y : α), x ≠ y → (∃ (U V : set α), is_open U ∧ is_open V ∧ disjoint (closure U) (closure V) ∧ x ∈ U ∧ y ∈ V)
A T₂.₅ space, also known as a Urysohn space, is a topological space
where for every pair x ≠ y
, there are two open sets, with the intersection of closures
empty, one containing x
and the other y
.
Instances of this typeclass
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.
t2_space
constructions #
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 thatf x ≠ f y
. We use this lemma to prove that topological spaces defined usinginduced
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
. See also
set.eq_on.of_subset_closure
for a more general version.
If two continuous functions are equal on a dense set, then they are equal.
If f x = g x
for all x ∈ s
and f
, g
are continuous on t
, s ⊆ t ⊆ closure s
, then
f x = g x
for all x ∈ t
. See also set.eq_on.closure
.
In a t2_space
, every compact set is closed.
If V : ι → set α
is a decreasing family of compact sets then any neighborhood of
⋂ i, V i
contains some V i
. This is a version of exists_subset_nhd_of_compact'
where we
don't need to assume each V i
closed because it follows from compactness since α
is
assumed to be Hausdorff.
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
In a locally compact T₂ space, every compact set has an open neighborhood with compact closure.
In a locally compact T₂ space, given a compact set K
inside an open set U
, we can find a
open set V
between these sets with compact closure: K ⊆ V
and the closure of V
is inside U
.
- to_t0_space : t0_space α
- regular : ∀ {s : set α} {a : α}, is_closed s → a ∉ s → (∃ (t : set α), is_open t ∧ s ⊆ t ∧ nhds_within a t = ⊥)
A T₃ space is a T₀ space in which for every closed C
and x ∉ C
, there exist
disjoint open sets containing x
and C
respectively.
Instances of this typeclass
Given two points x ≠ y
, we can find neighbourhoods x ∈ V₁ ⊆ U₁
and y ∈ V₂ ⊆ U₂
,
with the Vₖ
closed and the Uₖ
open, such that the Uₖ
are disjoint.
- 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 of this typeclass
A T₃ topological space with second countable topology is a normal space. This lemma is not an instance to avoid a loop.
In a compact t2 space, the connected component of a point equals the intersection of all its clopen neighbourhoods.
A Hausdorff space with a clopen basis is totally separated.
A compact Hausdorff space is totally disconnected if and only if it is totally separated, this is also true for locally compact spaces.
Every member of an open set in a compact Hausdorff totally disconnected space is contained in a clopen set contained in the open set.
A locally compact Hausdorff totally disconnected space has a basis with clopen elements.
A locally compact Hausdorff space is totally disconnected if and only if it is totally separated.
connected_components α
is Hausdorff when α
is Hausdorff and compact