Totally disconnected and totally separated topological spaces #
Main definitions #
We define the following properties for sets in a topological space:
IsTotallyDisconnected: all of its connected components are singletons.IsTotallySeparated: any two points can be separated by two disjoint opens that cover the set.
For both of these definitions, we also have a class stating that the whole space
satisfies that property: TotallyDisconnectedSpace, TotallySeparatedSpace.
A set s is called totally disconnected if every subset t ⊆ s which is preconnected is
a subsingleton, ie either empty or a singleton.
Equations
- IsTotallyDisconnected s = ∀ t ⊆ s, IsPreconnected t → t.Subsingleton
Instances For
A space is totally disconnected if all of its connected components are singletons.
- isTotallyDisconnected_univ : IsTotallyDisconnected Set.univ
The universal set
Set.univin a totally disconnected space is totally disconnected.
Instances
theorem
totallyDisconnectedSpace_iff
(α : Type u)
[TopologicalSpace α]
:
TotallyDisconnectedSpace α ↔ IsTotallyDisconnected Set.univ
theorem
IsPreconnected.subsingleton
{α : Type u}
[TopologicalSpace α]
[TotallyDisconnectedSpace α]
{s : Set α}
(h : IsPreconnected s)
:
s.Subsingleton
instance
Pi.totallyDisconnectedSpace
{α : Type u_3}
{β : α → Type u_4}
[(a : α) → TopologicalSpace (β a)]
[∀ (a : α), TotallyDisconnectedSpace (β a)]
:
TotallyDisconnectedSpace ((a : α) → β a)
instance
Prod.totallyDisconnectedSpace
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[TotallyDisconnectedSpace α]
[TotallyDisconnectedSpace β]
:
TotallyDisconnectedSpace (α × β)
instance
instTotallyDisconnectedSpaceSum
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[TotallyDisconnectedSpace α]
[TotallyDisconnectedSpace β]
:
TotallyDisconnectedSpace (α ⊕ β)
instance
instTotallyDisconnectedSpaceSigma
{ι : Type u_1}
{π : ι → Type u_2}
[(i : ι) → TopologicalSpace (π i)]
[∀ (i : ι), TotallyDisconnectedSpace (π i)]
:
TotallyDisconnectedSpace ((i : ι) × π i)
theorem
isTotallyDisconnected_of_isClopen_set
{X : Type u_3}
[TopologicalSpace X]
(hX : Pairwise fun (x y : X) => ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∉ U)
:
IsTotallyDisconnected Set.univ
Let X be a topological space, and suppose that for all distinct x,y ∈ X, there
is some clopen set U such that x ∈ U and y ∉ U. Then X is totally disconnected.
theorem
totallyDisconnectedSpace_iff_connectedComponent_subsingleton
{α : Type u}
[TopologicalSpace α]
:
TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton
A space is totally disconnected iff its connected components are subsingletons.
theorem
totallyDisconnectedSpace_iff_connectedComponent_singleton
{α : Type u}
[TopologicalSpace α]
:
TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}
A space is totally disconnected iff its connected components are singletons.
@[simp]
theorem
connectedComponent_eq_singleton
{α : Type u}
[TopologicalSpace α]
[TotallyDisconnectedSpace α]
(x : α)
:
connectedComponent x = {x}
@[simp]
theorem
Continuous.image_connectedComponent_eq_singleton
{α : Type u}
[TopologicalSpace α]
{β : Type u_3}
[TopologicalSpace β]
[TotallyDisconnectedSpace β]
{f : α → β}
(h : Continuous f)
(a : α)
:
f '' connectedComponent a = {f a}
The image of a connected component in a totally disconnected space is a singleton.
theorem
isTotallyDisconnected_of_totallyDisconnectedSpace
{α : Type u}
[TopologicalSpace α]
[TotallyDisconnectedSpace α]
(s : Set α)
:
theorem
isTotallyDisconnected_of_image
{α : Type u}
{β : Type v}
[TopologicalSpace α]
{s : Set α}
[TopologicalSpace β]
{f : α → β}
(hf : ContinuousOn f s)
(hf' : Function.Injective f)
(h : IsTotallyDisconnected (f '' s))
:
theorem
Topology.IsEmbedding.isTotallyDisconnected
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
(hf : Topology.IsEmbedding f)
(h : IsTotallyDisconnected (f '' s))
:
@[deprecated Topology.IsEmbedding.isTotallyDisconnected]
theorem
Embedding.isTotallyDisconnected
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
(hf : Topology.IsEmbedding f)
(h : IsTotallyDisconnected (f '' s))
:
theorem
Topology.IsEmbedding.isTotallyDisconnected_image
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
(hf : Topology.IsEmbedding f)
:
@[deprecated Topology.IsEmbedding.isTotallyDisconnected_image]
theorem
Embedding.isTotallyDisconnected_image
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
(hf : Topology.IsEmbedding f)
:
theorem
Topology.IsEmbedding.isTotallyDisconnected_range
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Topology.IsEmbedding f)
:
@[deprecated Topology.IsEmbedding.isTotallyDisconnected_range]
theorem
Embedding.isTotallyDisconnected_range
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Topology.IsEmbedding f)
:
instance
Subtype.totallyDisconnectedSpace
{α : Type u_3}
{p : α → Prop}
[TopologicalSpace α]
[TotallyDisconnectedSpace α]
:
A set s is called totally separated if any two points of this set can be separated
by two disjoint open sets covering s.
Equations
Instances For
theorem
isTotallyDisconnected_of_isTotallySeparated
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(H : IsTotallySeparated s)
:
theorem
IsTotallySeparated.isTotallyDisconnected
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(H : IsTotallySeparated s)
:
A space is totally separated if any two points can be separated by two disjoint open sets covering the whole space.
- isTotallySeparated_univ : IsTotallySeparated Set.univ
The universal set
Set.univin a totally separated space is totally separated.
Instances
theorem
totallySeparatedSpace_iff
(α : Type u)
[TopologicalSpace α]
:
TotallySeparatedSpace α ↔ IsTotallySeparated Set.univ
@[instance 100]
instance
TotallySeparatedSpace.totallyDisconnectedSpace
(α : Type u)
[TopologicalSpace α]
[TotallySeparatedSpace α]
:
@[instance 100]
instance
TotallySeparatedSpace.of_discrete
(α : Type u_3)
[TopologicalSpace α]
[DiscreteTopology α]
:
theorem
exists_isClopen_of_totally_separated
{α : Type u_3}
[TopologicalSpace α]
[TotallySeparatedSpace α]
{x y : α}
(hxy : x ≠ y)
:
theorem
Continuous.image_eq_of_connectedComponent_eq
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[TotallyDisconnectedSpace β]
{f : α → β}
(h : Continuous f)
(a b : α)
(hab : connectedComponent a = connectedComponent b)
:
f a = f b
def
Continuous.connectedComponentsLift
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[TotallyDisconnectedSpace β]
{f : α → β}
(h : Continuous f)
:
ConnectedComponents α → β
The lift to connectedComponents α of a continuous map from α to a totally disconnected space
Equations
- h.connectedComponentsLift x = Quotient.liftOn' x f ⋯
Instances For
theorem
Continuous.connectedComponentsLift_continuous
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[TotallyDisconnectedSpace β]
{f : α → β}
(h : Continuous f)
:
Continuous h.connectedComponentsLift
@[simp]
theorem
Continuous.connectedComponentsLift_apply_coe
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[TotallyDisconnectedSpace β]
{f : α → β}
(h : Continuous f)
(x : α)
:
h.connectedComponentsLift (ConnectedComponents.mk x) = f x
@[simp]
theorem
Continuous.connectedComponentsLift_comp_coe
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[TotallyDisconnectedSpace β]
{f : α → β}
(h : Continuous f)
:
theorem
connectedComponents_lift_unique'
{α : Type u}
[TopologicalSpace α]
{β : Sort u_3}
{g₁ g₂ : ConnectedComponents α → β}
(hg : g₁ ∘ ConnectedComponents.mk = g₂ ∘ ConnectedComponents.mk)
:
g₁ = g₂
theorem
Continuous.connectedComponentsLift_unique
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[TotallyDisconnectedSpace β]
{f : α → β}
(h : Continuous f)
(g : ConnectedComponents α → β)
(hg : g ∘ ConnectedComponents.mk = f)
:
g = h.connectedComponentsLift
def
Continuous.connectedComponentsMap
{α : Type u}
[TopologicalSpace α]
{β : Type u_3}
[TopologicalSpace β]
{f : α → β}
(h : Continuous f)
:
Functoriality of connectedComponents
Equations
- h.connectedComponentsMap = ⋯.connectedComponentsLift
Instances For
theorem
Continuous.connectedComponentsMap_continuous
{α : Type u}
[TopologicalSpace α]
{β : Type u_3}
[TopologicalSpace β]
{f : α → β}
(h : Continuous f)
:
Continuous h.connectedComponentsMap
theorem
IsPreconnected.constant
{α : Type u}
[TopologicalSpace α]
{Y : Type u_3}
[TopologicalSpace Y]
[DiscreteTopology Y]
{s : Set α}
(hs : IsPreconnected s)
{f : α → Y}
(hf : ContinuousOn f s)
{x y : α}
(hx : x ∈ s)
(hy : y ∈ s)
:
f x = f y
A preconnected set s has the property that every map to a
discrete space that is continuous on s is constant on s
theorem
PreconnectedSpace.constant
{α : Type u}
[TopologicalSpace α]
{Y : Type u_3}
[TopologicalSpace Y]
[DiscreteTopology Y]
(hp : PreconnectedSpace α)
{f : α → Y}
(hf : Continuous f)
{x y : α}
:
f x = f y
A PreconnectedSpace version of isPreconnected.constant
theorem
IsPreconnected.constant_of_mapsTo
{α : Type u}
[TopologicalSpace α]
{S : Set α}
(hS : IsPreconnected S)
{β : Type u_3}
[TopologicalSpace β]
{T : Set β}
[DiscreteTopology ↑T]
{f : α → β}
(hc : ContinuousOn f S)
(hTm : Set.MapsTo f S T)
{x y : α}
(hx : x ∈ S)
(hy : y ∈ S)
:
f x = f y
Refinement of IsPreconnected.constant only assuming the map factors through a
discrete subset of the target.
theorem
IsPreconnected.eqOn_const_of_mapsTo
{α : Type u}
[TopologicalSpace α]
{S : Set α}
(hS : IsPreconnected S)
{β : Type u_3}
[TopologicalSpace β]
{T : Set β}
[DiscreteTopology ↑T]
{f : α → β}
(hc : ContinuousOn f S)
(hTm : Set.MapsTo f S T)
(hne : T.Nonempty)
:
∃ y ∈ T, Set.EqOn f (Function.const α y) S
A version of IsPreconnected.constant_of_mapsTo that assumes that the codomain is nonempty and
proves that f is equal to const α y on S for some y ∈ T.