Path connectedness

Continuing from Mathlib.Topology.Path, 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.

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

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

@[deprecated Topology.IsInducing.joinedIn_image (since := "2024-10-28")]

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

Alias of Topology.IsInducing.joinedIn_image.

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] (x : X) (F : Set 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 x F = {y : X | JoinedIn F x y}

@[simp]

theorem pathComponentIn_univ {X : Type u_1} [TopologicalSpace X] (x : X) : pathComponentIn x Set.univ = 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 x F

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

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

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

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

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 x F = 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 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.

@[deprecated Topology.IsInducing.isPathConnected_iff (since := "2024-10-28")]

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

Alias of Topology.IsInducing.isPathConnected_iff.

---

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 x F

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 x F)

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 ↑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 ↑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

theorem PathConnectedSpace.exists_path_through_family {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] {n : ℕ} (p : Fin (n + 1) → X) : ∃ (γ : Path (p 0) (p ↑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 ↑n)) (t : Fin (n + 1) → ↑unitInterval), ∀ (i : Fin (n + 1)), γ (t i) = p i