theorem IsConnected.subset_connectedComponent_of_mem {X : Type u_1} [TopologicalSpace X] {x y : X} {s : Set X} (hs : IsConnected s) (ys : y ∈ s) (xy : y ∈ connectedComponent x) : s ⊆ connectedComponent x

If s is a connected set containing y and y lies in the connected component of y, s is contained in the connected component of x.

theorem PiBase.HasOpenConnectedComponents.connectedComponent_nbhd {X : Type u_1} [TopologicalSpace X] [HasOpenConnectedComponents X] (x : X) : connectedComponent x ∈ nhds x

theorem PiBase.HasOpenConnectedComponents.connectedComponent_isClopen {X : Type u_1} [TopologicalSpace X] [h : HasOpenConnectedComponents X] (x : X) : IsClopen (connectedComponent x)

In a space with open connected components, every connected component is clopen.

theorem PiBase.hasOpenConnectedComponents_iff_ex_connected_nbhd (X : Type u_1) [TopologicalSpace X] : HasOpenConnectedComponents X ↔ ∀ (x : X), ∃ s ∈ nhds x, IsConnected s

A space has open connected components iff each point has a connected neighborhood.

theorem PiBase.WellDefined.hasOpenConnectedComponents : WellDefined fun (X : Type u) [TopologicalSpace X] => HasOpenConnectedComponents X