class PiBase.TotallyPathDisconnectedSpace (X : Type u_1) [TopologicalSpace X] : Prop

• totally_path_disconnected (f : ↑(Set.Icc 0 1) → X) : Continuous f → ∃ (x : X), f = Function.const (↑(Set.Icc 0 1)) x