theorem IsPathConnected.subset_pathComponent_of_mem {X : Type u_1} [TopologicalSpace X] {x y : X} {s : Set X} (hs : IsPathConnected s) (ys : y ∈ s) (xy : y ∈ pathComponent x) : s ⊆ pathComponent x

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

theorem PathconnectedSpace.connectedComponent_eq_univ {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (x : X) : pathComponent x = Set.univ

In a path connected space, all path components are the entire space.

theorem pathComponent_eq_iff_joined {X : Type u_1} [TopologicalSpace X] (x y : X) : pathComponent x = pathComponent y ↔ Joined x y

Two points are joined iff there path components are the same.

theorem PiBase.HasOpenPathComponents.pathComponent_nbhd {X : Type u_1} [TopologicalSpace X] [HasOpenPathComponents X] (x : X) : pathComponent x ∈ nhds x

theorem pathComponent_disjoint {X : Type u_1} [TopologicalSpace X] {x y : X} (h : pathComponent x ≠ pathComponent y) : Disjoint (pathComponent x) (pathComponent y)

Two different path components are disjoint.

theorem PiBase.HasOpenPathComponents.pathComponent_isClopen {X : Type u_1} [TopologicalSpace X] [h : HasOpenPathComponents X] (x : X) : IsClopen (pathComponent x)

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

theorem PiBase.hasOpenPathComponents_iff_ex_connected_nbhd (X : Type u_1) [TopologicalSpace X] : HasOpenPathComponents X ↔ ∀ (x : X), ∃ s ∈ nhds x, IsPathConnected s

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

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