Total disconnectedness of finite sets and of a universe lift #
In a T₁ space every finite set is discrete, hence totally disconnected, since a preconnected
discrete set has at most one point. This is how a finite ω-limit set is shown to be a single point.
The universe lift ULift X of a topological space is homeomorphic to X
(Homeomorph.ulift), so it is totally disconnected when X is. Mathlib records the analogous
transport for compactness (ULift.compactSpace); this instance completes the profinite instance
stack on ULift X, which the universal properties of free pro-p groups need when a target group
has to be lifted to the universe of the generating set.
theorem
Set.Finite.isTotallyDisconnected
{X : Type u_1}
[TopologicalSpace X]
[T1Space X]
{s : Set X}
(hs : s.Finite)
:
A finite set in a T₁ space is totally disconnected.
instance
ULift.totallyDisconnectedSpace
{X : Type u}
[TopologicalSpace X]
[TotallyDisconnectedSpace X]
:
The universe lift of a totally disconnected space is totally disconnected.