Separation properties of topological spaces. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the predicate separated_nhds
, and common separation axioms
(under the Kolmogorov classification).
Main definitions #
separated_nhds
: Twoset
s are separated by neighbourhoods 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₃.t5_space
: A T₅ space, also known as a completely normal Hausdorff space
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_nhds
.- 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.totally_separated_space_of_t1_of_basis_clopen
: Ifα
has a clopen basis, then 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.
References #
separated_nhds
is a predicate on pairs of subset
s of a topological space. It holds if the two
subset
s are contained in disjoint open sets.
- 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.
Instances of this typeclass
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.
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
.
Instances of this typeclass
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 := _}
If t
is a subset of s
, except for one point,
then insert x s
is a neighborhood of x
within t
.
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
.
A point with a finite neighborhood has to be isolated.
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
.
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
- t2_space_of_properly_discontinuous_smul_of_t2_space
- t2_space_of_properly_discontinuous_vadd_of_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
- uniform_fun.t2_space
- ennreal.t2_space
- continuous_map.t2_space
- continuous_linear_map.t2_space
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.
A continuous map from a compact space to a Hausdorff space is a closed map.
An injective continuous map from a compact space to a Hausdorff space is a closed embedding.
A surjective continuous map from a compact space to a Hausdorff space is a quotient map.
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
.
Alias of the forward direction of is_preirreducible_iff_subsingleton
.
There does not exist a nontrivial preirreducible T₂ space.
A topological space is called a regular space if for any closed set s
and a ∉ s
, there
exist disjoint open sets U ⊇ s
and V ∋ a
. We formulate this condition in terms of disjoint
ness
of filters 𝓝ˢ s
and 𝓝 a
.
Alias of the forward direction of specializes_comm
.
- to_t0_space : t0_space α
- to_regular_space : regular_space α
A T₃ space is a T₀ space which is a regular space. Any T₃ space is a T₁ space, a T₂ space, and a T₂.₅ space.
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.
The separation_quotient
of a regular space is a T₃ space.
- to_t1_space : t1_space α
- normal : ∀ (s t : set α), is_closed s → is_closed t → disjoint s t → separated_nhds s t
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
The separation_quotient
of a normal space is a T₄ space. We don't have separate typeclasses
for normal spaces (without T₁ assumption) and T₄ spaces, so we use the same class for assumption
and for conclusion.
One can prove this using a homeomorphism between α
and separation_quotient α
. We give an
alternative proof that works without assuming that α
is a T₁ space.
A T₃ topological space with second countable topology is a normal space. This lemma is not an instance to avoid a loop.
- to_t1_space : t1_space α
- completely_normal : ∀ ⦃s t : set α⦄, disjoint (closure s) t → disjoint s (closure t) → disjoint (nhds_set s) (nhds_set t)
A topological space α
is a completely normal Hausdorff space if each subspace s : set α
is
a normal Hausdorff space. Equivalently, α
is a T₁
space and for any two sets s
, t
such that
closure s
is disjoint with t
and s
is disjoint with closure t
, there exist disjoint
neighbourhoods of s
and t
.
Instances of this typeclass
A subspace of a T₅
space is a T₅
space.
A T₅
space is a T₄
space.
The separation_quotient
of a completely normal space is a T₅ space. We don't have separate
typeclasses for completely normal spaces (without T₁ assumption) and T₅ spaces, so we use the same
class for assumption and for conclusion.
One can prove this using a homeomorphism between α
and separation_quotient α
. We give an
alternative proof that works without assuming that α
is a T₁ space.
In a compact t2 space, the connected component of a point equals the intersection of all its clopen neighbourhoods.
A T1 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