theorem PiBase.totallyPathDisconnectedSpace_iff_joined (X : Type u_1) [TopologicalSpace X] : TotallyPathDisconnectedSpace X ↔ ∀ ⦃x y : X⦄, Joined x y → x = y

A space is totally path disconnected iff all no two different point are joined.

theorem PiBase.totallyPathDisconnectedSpace_iff_pathComponent_singleton (X : Type u_1) [TopologicalSpace X] : TotallyPathDisconnectedSpace X ↔ ∀ (x : X), pathComponent x = {x}

A space is totally path disconnected iff all of its path components are singletons.

theorem PiBase.WellDefined.totallyPathDisconnectedSpace : WellDefined TotallyPathDisconnectedSpace