Path connectedness

Continuing from Mathlib/Topology/Path.lean, this file defines path components and path-connected spaces.

Main definitions

In the file the unit interval [0, 1] in ℝ is denoted by I, and X is a topological space.

• Joined (x y : X) means there is a path between x and y.
• Joined.somePath (h : Joined x y) selects some path between two points x and y.
• pathComponent (x : X) is the set of points joined to x.
• PathConnectedSpace X is a predicate class asserting that X is non-empty and every two points of X are joined.

Then there are corresponding relative notions for F : Set X.

• JoinedIn F (x y : X) means there is a path γ joining x to y with values in F.
• JoinedIn.somePath (h : JoinedIn F x y) selects a path from x to y inside F.
• pathComponentIn F (x : X) is the set of points joined to x in F.
• IsPathConnected F asserts that F is non-empty and every two points of F are joined in F.

Main theorems

• Joined is an equivalence relation, while JoinedIn F is at least symmetric and transitive.

One can link the absolute and relative version in two directions, using (univ : Set X) or the subtype ↥F.

• pathConnectedSpace_iff_univ : PathConnectedSpace X ↔ IsPathConnected (univ : Set X)
• isPathConnected_iff_pathConnectedSpace : IsPathConnected F ↔ PathConnectedSpace ↥F

Furthermore, it is shown that continuous images and quotients of path-connected sets/spaces are path-connected, and that every path-connected set/space is also connected. (See Counterexamples.TopologistsSineCurve for an example of a set in ℝ × ℝ that is connected but not path-connected.)

Being joined by a path

def Joined {X : Type u_1} [TopologicalSpace X] (x y : X) : Prop

The relation "being joined by a path". This is an equivalence relation.

Equations

• Joined x y = Nonempty (Path x y)

theorem Joined.refl {X : Type u_1} [TopologicalSpace X] (x : X) : Joined x x

def Joined.somePath {X : Type u_1} [TopologicalSpace X] {x y : X} (h : Joined x y) : Path x y

When two points are joined, choose some path from x to y.

Equations

• h.somePath = Nonempty.some h

theorem Joined.symm {X : Type u_1} [TopologicalSpace X] {x y : X} (h : Joined x y) : Joined y x

theorem Joined.trans {X : Type u_1} [TopologicalSpace X] {x y z : X} (hxy : Joined x y) (hyz : Joined y z) : Joined x z

theorem Joined.mul {M : Type u_4} [Mul M] [TopologicalSpace M] [ContinuousMul M] {a b c d : M} (hs : Joined a b) (ht : Joined c d) : Joined (a * c) (b * d)

theorem Joined.add {M : Type u_4} [Add M] [TopologicalSpace M] [ContinuousAdd M] {a b c d : M} (hs : Joined a b) (ht : Joined c d) : Joined (a + c) (b + d)

theorem Joined.listProd {M : Type u_4} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] {l l' : List M} (h : List.Forall₂ Joined l l') : Joined l.prod l'.prod

theorem Joined.listSum {M : Type u_4} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] {l l' : List M} (h : List.Forall₂ Joined l l') : Joined l.sum l'.sum

theorem Joined.inv {G : Type u_4} [Inv G] [TopologicalSpace G] [ContinuousInv G] {x y : G} (h : Joined x y) : Joined x⁻¹ y⁻¹

theorem Joined.neg {G : Type u_4} [Neg G] [TopologicalSpace G] [ContinuousNeg G] {x y : G} (h : Joined x y) : Joined (-x) (-y)

def pathSetoid (X : Type u_1) [TopologicalSpace X] : Setoid X

The setoid corresponding the equivalence relation of being joined by a continuous path.

Equations

• pathSetoid X = { r := Joined, iseqv := ⋯ }

def ZerothHomotopy (X : Type u_1) [TopologicalSpace X] : Type u_1

The quotient type of points of a topological space modulo being joined by a continuous path.

Equations

• ZerothHomotopy X = Quotient (pathSetoid X)

instance ZerothHomotopy.inhabited : Inhabited (ZerothHomotopy ℝ)

Equations

• ZerothHomotopy.inhabited = { default := Quotient.mk' 0 }

Being joined by a path inside a set

def JoinedIn {X : Type u_1} [TopologicalSpace X] (F : Set X) (x y : X) : Prop

The relation "being joined by a path in F". Not quite an equivalence relation since it's not reflexive for points that do not belong to F.

Equations

• JoinedIn F x y = ∃ (γ : Path x y), ∀ (t : ↑unitInterval), γ t ∈ F

theorem JoinedIn.mem {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y) : x ∈ F ∧ y ∈ F

theorem JoinedIn.source_mem {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y) : x ∈ F

theorem JoinedIn.target_mem {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y) : y ∈ F

def JoinedIn.somePath {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y) : Path x y

When x and y are joined in F, choose a path from x to y inside F

Equations

• h.somePath = Classical.choose h

theorem JoinedIn.somePath_mem {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y) (t : ↑unitInterval) : h.somePath t ∈ F

theorem JoinedIn.joined_subtype {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y) : Joined ⟨x, ⋯⟩ ⟨y, ⋯⟩

If x and y are joined in the set F, then they are joined in the subtype F.

theorem JoinedIn.ofLine {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} {f : ℝ → X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x) (h₁ : f 1 = y) (hF : f '' unitInterval ⊆ F) : JoinedIn F x y

theorem JoinedIn.joined {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y) : Joined x y

theorem joinedIn_iff_joined {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (x_in : x ∈ F) (y_in : y ∈ F) : JoinedIn F x y ↔ Joined ⟨x, x_in⟩ ⟨y, y_in⟩

@[simp]

theorem joinedIn_univ {X : Type u_1} [TopologicalSpace X] {x y : X} : JoinedIn Set.univ x y ↔ Joined x y

theorem JoinedIn.mono {X : Type u_1} [TopologicalSpace X] {x y : X} {U V : Set X} (h : JoinedIn U x y) (hUV : U ⊆ V) : JoinedIn V x y

theorem JoinedIn.refl {X : Type u_1} [TopologicalSpace X] {x : X} {F : Set X} (h : x ∈ F) : JoinedIn F x x

theorem JoinedIn.symm {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y) : JoinedIn F y x

theorem JoinedIn.trans {X : Type u_1} [TopologicalSpace X] {x y z : X} {F : Set X} (hxy : JoinedIn F x y) (hyz : JoinedIn F y z) : JoinedIn F x z

theorem Specializes.joinedIn {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : x ⤳ y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y

theorem Inseparable.joinedIn {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : Inseparable x y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y

theorem JoinedIn.map_continuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {F : Set X} (h : JoinedIn F x y) {f : X → Y} (hf : ContinuousOn f F) : JoinedIn (f '' F) (f x) (f y)

theorem JoinedIn.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {F : Set X} (h : JoinedIn F x y) {f : X → Y} (hf : Continuous f) : JoinedIn (f '' F) (f x) (f y)

theorem Topology.IsInducing.joinedIn_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {F : Set X} {f : X → Y} (hf : IsInducing f) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y

theorem JoinedIn.mul {M : Type u_4} [Mul M] [TopologicalSpace M] [ContinuousMul M] {s t : Set M} {a b c d : M} (hs : JoinedIn s a b) (ht : JoinedIn t c d) : JoinedIn (s * t) (a * c) (b * d)

theorem JoinedIn.add {M : Type u_4} [Add M] [TopologicalSpace M] [ContinuousAdd M] {s t : Set M} {a b c d : M} (hs : JoinedIn s a b) (ht : JoinedIn t c d) : JoinedIn (s + t) (a + c) (b + d)

theorem JoinedIn.inv {G : Type u_4} [InvolutiveInv G] [TopologicalSpace G] [ContinuousInv G] {s : Set G} {a b : G} (hs : JoinedIn s a b) : JoinedIn s⁻¹ a⁻¹ b⁻¹

theorem JoinedIn.neg {G : Type u_4} [InvolutiveNeg G] [TopologicalSpace G] [ContinuousNeg G] {s : Set G} {a b : G} (hs : JoinedIn s a b) : JoinedIn (-s) (-a) (-b)

Path component

def pathComponent {X : Type u_1} [TopologicalSpace X] (x : X) : Set X

The path component of x is the set of points that can be joined to x.

Equations

• pathComponent x = {y : X | Joined x y}

theorem mem_pathComponent_iff {X : Type u_1} [TopologicalSpace X] {x y : X} : x ∈ pathComponent y ↔ Joined y x

@[simp]

theorem mem_pathComponent_self {X : Type u_1} [TopologicalSpace X] (x : X) : x ∈ pathComponent x

@[simp]

theorem pathComponent.nonempty {X : Type u_1} [TopologicalSpace X] (x : X) : (pathComponent x).Nonempty

theorem mem_pathComponent_of_mem {X : Type u_1} [TopologicalSpace X] {x y : X} (h : x ∈ pathComponent y) : y ∈ pathComponent x

theorem pathComponent_symm {X : Type u_1} [TopologicalSpace X] {x y : X} : x ∈ pathComponent y ↔ y ∈ pathComponent x

theorem pathComponent_congr {X : Type u_1} [TopologicalSpace X] {x y : X} (h : x ∈ pathComponent y) : pathComponent x = pathComponent y

theorem pathComponent_subset_component {X : Type u_1} [TopologicalSpace X] (x : X) : pathComponent x ⊆ connectedComponent x

def pathComponentIn {X : Type u_1} [TopologicalSpace X] (F : Set X) (x : X) : Set X

The path component of x in F is the set of points that can be joined to x in F.

Equations

• pathComponentIn F x = {y : X | JoinedIn F x y}

@[simp]

theorem pathComponentIn_univ {X : Type u_1} [TopologicalSpace X] (x : X) : pathComponentIn Set.univ x = pathComponent x

theorem Joined.mem_pathComponent {X : Type u_1} [TopologicalSpace X] {x y z : X} (hyz : Joined y z) (hxy : y ∈ pathComponent x) : z ∈ pathComponent x

theorem mem_pathComponentIn_self {X : Type u_1} [TopologicalSpace X] {x : X} {F : Set X} (h : x ∈ F) : x ∈ pathComponentIn F x

theorem pathComponentIn_subset {X : Type u_1} [TopologicalSpace X] {x : X} {F : Set X} : pathComponentIn F x ⊆ F

theorem pathComponentIn_nonempty_iff {X : Type u_1} [TopologicalSpace X] {x : X} {F : Set X} : (pathComponentIn F x).Nonempty ↔ x ∈ F

theorem pathComponentIn_congr {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : x ∈ pathComponentIn F y) : pathComponentIn F x = pathComponentIn F y

theorem pathComponentIn_mono {X : Type u_1} [TopologicalSpace X] {x : X} {F G : Set X} (h : F ⊆ G) : pathComponentIn F x ⊆ pathComponentIn G x

Path component of the identity in a group

def Submonoid.pathComponentOne (M : Type u_4) [Monoid M] [TopologicalSpace M] [ContinuousMul M] : Submonoid M

The path component of the identity in a topological monoid, as a submonoid.

Equations

• Submonoid.pathComponentOne M = { carrier := pathComponent 1, mul_mem' := ⋯, one_mem' := ⋯ }

def AddSubmonoid.pathComponentZero (M : Type u_4) [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] : AddSubmonoid M

The path component of the identity in an additive topological monoid, as an additive submonoid.

Equations

• AddSubmonoid.pathComponentZero M = { carrier := pathComponent 0, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem AddSubmonoid.coe_pathComponentZero (M : Type u_4) [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] : ↑(pathComponentZero M) = pathComponent 0

@[simp]

theorem Submonoid.coe_pathComponentOne (M : Type u_4) [Monoid M] [TopologicalSpace M] [ContinuousMul M] : ↑(pathComponentOne M) = pathComponent 1

def Subgroup.pathComponentOne (G : Type u_4) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Subgroup G

The path component of the identity in a topological group, as a subgroup.

Equations

• Subgroup.pathComponentOne G = { toSubmonoid := Submonoid.pathComponentOne G, inv_mem' := ⋯ }

def AddSubgroup.pathComponentZero (G : Type u_4) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : AddSubgroup G

The path component of the identity in an additive topological group, as an additive subgroup.

Equations

• AddSubgroup.pathComponentZero G = { toAddSubmonoid := AddSubmonoid.pathComponentZero G, neg_mem' := ⋯ }

@[simp]

theorem Subgroup.coe_pathComponentOne (G : Type u_4) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ↑(pathComponentOne G) = pathComponent 1

@[simp]

theorem AddSubgroup.coe_pathComponentZero (G : Type u_4) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : ↑(pathComponentZero G) = pathComponent 0

instance Subgroup.Normal.pathComponentOne (G : Type u_4) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (Subgroup.pathComponentOne G).Normal

The path component of the identity in a topological group is normal.

instance AddSubgroup.Normal.pathComponentZero (G : Type u_4) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : (AddSubgroup.pathComponentZero G).Normal

Path connected sets

def IsPathConnected {X : Type u_1} [TopologicalSpace X] (F : Set X) : Prop

A set F is path connected if it contains a point that can be joined to all other in F.

Equations

• IsPathConnected F = ∃ x ∈ F, ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y

theorem isPathConnected_iff_eq {X : Type u_1} [TopologicalSpace X] {F : Set X} : IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F

theorem IsPathConnected.joinedIn {X : Type u_1} [TopologicalSpace X] {F : Set X} (h : IsPathConnected F) (x : X) : x ∈ F → ∀ y ∈ F, JoinedIn F x y

theorem isPathConnected_iff {X : Type u_1} [TopologicalSpace X] {F : Set X} : IsPathConnected F ↔ F.Nonempty ∧ ∀ x ∈ F, ∀ y ∈ F, JoinedIn F x y

theorem IsPathConnected.image' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Set X} (hF : IsPathConnected F) {f : X → Y} (hf : ContinuousOn f F) : IsPathConnected (f '' F)

If f is continuous on F and F is path-connected, so is f(F).

theorem IsPathConnected.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Set X} (hF : IsPathConnected F) {f : X → Y} (hf : Continuous f) : IsPathConnected (f '' F)

If f is continuous and F is path-connected, so is f(F).

theorem IsPathConnected.mul {M : Type u_4} [Mul M] [TopologicalSpace M] [ContinuousMul M] {s t : Set M} (hs : IsPathConnected s) (ht : IsPathConnected t) : IsPathConnected (s * t)

theorem IsPathConnected.add {M : Type u_4} [Add M] [TopologicalSpace M] [ContinuousAdd M] {s t : Set M} (hs : IsPathConnected s) (ht : IsPathConnected t) : IsPathConnected (s + t)

theorem IsPathConnected.inv {G : Type u_4} [InvolutiveInv G] [TopologicalSpace G] [ContinuousInv G] {s : Set G} (hs : IsPathConnected s) : IsPathConnected s⁻¹

theorem IsPathConnected.neg {G : Type u_4} [InvolutiveNeg G] [TopologicalSpace G] [ContinuousNeg G] {s : Set G} (hs : IsPathConnected s) : IsPathConnected (-s)

theorem Topology.IsInducing.isPathConnected_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Set X} {f : X → Y} (hf : IsInducing f) : IsPathConnected F ↔ IsPathConnected (f '' F)

If f : X → Y is an inducing map, f(F) is path-connected iff F is.

@[simp]

theorem Homeomorph.isPathConnected_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) : IsPathConnected (⇑h '' s) ↔ IsPathConnected s

If h : X → Y is a homeomorphism, h(s) is path-connected iff s is.

@[simp]

theorem Homeomorph.isPathConnected_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y) : IsPathConnected (⇑h ⁻¹' s) ↔ IsPathConnected s

If h : X → Y is a homeomorphism, h⁻¹(s) is path-connected iff s is.

theorem IsPathConnected.mem_pathComponent {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : IsPathConnected F) (x_in : x ∈ F) (y_in : y ∈ F) : y ∈ pathComponent x

theorem IsPathConnected.subset_pathComponent {X : Type u_1} [TopologicalSpace X] {x : X} {F : Set X} (h : IsPathConnected F) (x_in : x ∈ F) : F ⊆ pathComponent x

theorem IsPathConnected.subset_pathComponentIn {X : Type u_1} [TopologicalSpace X] {x : X} {F s : Set X} (hs : IsPathConnected s) (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ pathComponentIn F x

theorem isPathConnected_singleton {X : Type u_1} [TopologicalSpace X] (x : X) : IsPathConnected {x}

theorem isPathConnected_pathComponentIn {X : Type u_1} [TopologicalSpace X] {x : X} {F : Set X} (h : x ∈ F) : IsPathConnected (pathComponentIn F x)

theorem isPathConnected_pathComponent {X : Type u_1} [TopologicalSpace X] {x : X} : IsPathConnected (pathComponent x)

theorem IsPathConnected.union {X : Type u_1} [TopologicalSpace X] {U V : Set X} (hU : IsPathConnected U) (hV : IsPathConnected V) (hUV : (U ∩ V).Nonempty) : IsPathConnected (U ∪ V)

theorem IsPathConnected.preimage_coe {X : Type u_1} [TopologicalSpace X] {U W : Set X} (hW : IsPathConnected W) (hWU : W ⊆ U) : IsPathConnected (Subtype.val ⁻¹' W)

If a set W is path-connected, then it is also path-connected when seen as a set in a smaller ambient type U (when U contains W).

theorem IsPathConnected.exists_path_through_family {X : Type u_1} [TopologicalSpace X] {n : ℕ} {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1) → X) (hp : ∀ (i : Fin (n + 1)), p i ∈ s) : ∃ (γ : Path (p 0) (p (Fin.last n))), Set.range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ Set.range ⇑γ

theorem IsPathConnected.exists_path_through_family' {X : Type u_1} [TopologicalSpace X] {n : ℕ} {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1) → X) (hp : ∀ (i : Fin (n + 1)), p i ∈ s) : ∃ (γ : Path (p 0) (p (Fin.last n))) (t : Fin (n + 1) → ↑unitInterval), (∀ (t : ↑unitInterval), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i

Path connected spaces

class PathConnectedSpace (X : Type u_4) [TopologicalSpace X] : Prop

A topological space is path-connected if it is non-empty and every two points can be joined by a continuous path.

• nonempty : Nonempty X

  A path-connected space must be nonempty.

• joined (x y : X) : Joined x y

  Any two points in a path-connected space must be joined by a continuous path.

theorem pathConnectedSpace_iff (X : Type u_4) [TopologicalSpace X] : PathConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Joined x y

theorem pathConnectedSpace_iff_zerothHomotopy {X : Type u_1} [TopologicalSpace X] : PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

def PathConnectedSpace.somePath {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (x y : X) : Path x y

Use path-connectedness to build a path between two points.

Equations

• PathConnectedSpace.somePath x y = Nonempty.some ⋯

theorem pathConnectedSpace_iff_univ {X : Type u_1} [TopologicalSpace X] : PathConnectedSpace X ↔ IsPathConnected Set.univ

theorem isPathConnected_iff_pathConnectedSpace {X : Type u_1} [TopologicalSpace X] {F : Set X} : IsPathConnected F ↔ PathConnectedSpace ↑F

theorem isPathConnected_univ {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] : IsPathConnected Set.univ

theorem isPathConnected_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PathConnectedSpace X] {f : X → Y} (hf : Continuous f) : IsPathConnected (Set.range f)

theorem Function.Surjective.pathConnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PathConnectedSpace X] {f : X → Y} (hf : Surjective f) (hf' : Continuous f) : PathConnectedSpace Y

instance Quotient.instPathConnectedSpace {X : Type u_1} [TopologicalSpace X] {s : Setoid X} [PathConnectedSpace X] : PathConnectedSpace (Quotient s)

instance Real.instPathConnectedSpace : PathConnectedSpace ℝ

This is a special case of NormedSpace.instPathConnectedSpace (and IsTopologicalAddGroup.pathConnectedSpace). It exists only to simplify dependencies.

theorem pathConnectedSpace_iff_eq {X : Type u_1} [TopologicalSpace X] : PathConnectedSpace X ↔ ∃ (x : X), pathComponent x = Set.univ

@[instance 100]

instance PathConnectedSpace.connectedSpace {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] : ConnectedSpace X

theorem IsPathConnected.isConnected {X : Type u_1} [TopologicalSpace X] {F : Set X} (hF : IsPathConnected F) : IsConnected F

A path-connected set is connected.

(See Counterexamples.TopologistsSineCurve for the standard counterexample showing that the converse is false.)

theorem PathConnectedSpace.exists_path_through_family {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] {n : ℕ} (p : Fin (n + 1) → X) : ∃ (γ : Path (p 0) (p (Fin.last n))), ∀ (i : Fin (n + 1)), p i ∈ Set.range ⇑γ

theorem PathConnectedSpace.exists_path_through_family' {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] {n : ℕ} (p : Fin (n + 1) → X) : ∃ (γ : Path (p 0) (p (Fin.last n))) (t : Fin (n + 1) → ↑unitInterval), ∀ (i : Fin (n + 1)), γ (t i) = p i