doc-next-gen

Mathlib.Topology.Connected.PathConnected

Module docstring

{"# 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 ","### Being joined by a path inside a set ","### Path component ","### Path connected sets ","### Path connected spaces "}

Joined definition
(x y : X) : Prop
Full source 
/-- The relation "being joined by a path". This is an equivalence relation. -/
def Joined (x y : X) : Prop :=
  Nonempty (Path x y)
Path-connected relation between two points
Informal description
The relation $\text{Joined}(x, y)$ holds for two points $x$ and $y$ in a topological space $X$ if there exists a continuous path $\gamma : [0,1] \to X$ with $\gamma(0) = x$ and $\gamma(1) = y$. This defines an equivalence relation on $X$.
Joined.refl theorem
(x : X) : Joined x x
Full source 
@[refl]
theorem Joined.refl (x : X) : Joined x x :=
  ⟨Path.refl x⟩
Reflexivity of Path-Connectedness Relation
Informal description
For any point $x$ in a topological space $X$, the relation $\text{Joined}(x, x)$ holds, meaning there exists a continuous path from $x$ to itself.
Joined.somePath definition
(h : Joined x y) : Path x y
Full source 
/-- When two points are joined, choose some path from `x` to `y`. -/
def Joined.somePath (h : Joined x y) : Path x y :=
  Nonempty.some h
Selection of a path between two points
Informal description
Given a proof $h$ that two points $x$ and $y$ in a topological space $X$ are path-connected (i.e., $\text{Joined}(x, y)$ holds), the function selects some continuous path $\gamma : [0,1] \to X$ with $\gamma(0) = x$ and $\gamma(1) = y$.
Joined.symm theorem
{x y : X} (h : Joined x y) : Joined y x
Full source 
@[symm]
theorem Joined.symm {x y : X} (h : Joined x y) : Joined y x :=
  ⟨h.somePath.symm⟩
Symmetry of Path-Connectedness Relation
Informal description
For any two points $x$ and $y$ in a topological space $X$, if there exists a continuous path from $x$ to $y$ (i.e., $\text{Joined}(x,y)$ holds), then there also exists a continuous path from $y$ to $x$.
Joined.trans theorem
{x y z : X} (hxy : Joined x y) (hyz : Joined y z) : Joined x z
Full source 
@[trans]
theorem Joined.trans {x y z : X} (hxy : Joined x y) (hyz : Joined y z) : Joined x z :=
  ⟨hxy.somePath.trans hyz.somePath⟩
Transitivity of Path-Connectedness
Informal description
For any three points $x, y, z$ in a topological space $X$, if there exists a continuous path from $x$ to $y$ and a continuous path from $y$ to $z$, then there exists a continuous path from $x$ to $z$.
pathSetoid definition
: Setoid X
Full source 
/-- The setoid corresponding the equivalence relation of being joined by a continuous path. -/
def pathSetoid : Setoid X where
  r := Joined
  iseqv := Equivalence.mk Joined.refl Joined.symm Joined.trans
Path-connected equivalence relation
Informal description
The equivalence relation on a topological space $X$ where two points $x$ and $y$ are related if and only if there exists a continuous path connecting them. This relation is reflexive, symmetric, and transitive, making it an equivalence relation.
ZerothHomotopy definition
Full source 
/-- The quotient type of points of a topological space modulo being joined by a continuous path. -/
def ZerothHomotopy :=
  Quotient (pathSetoid X)
Zeroth homotopy (path-connected components)
Informal description
The quotient type of points in a topological space $X$ modulo the equivalence relation of being connected by a continuous path. This construction identifies points that are path-connected, effectively partitioning the space into its path-connected components.
JoinedIn definition
(F : Set X) (x y : X) : Prop
Full source 
/-- 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`. -/
def JoinedIn (F : Set X) (x y : X) : Prop :=
  ∃ γ : Path x y, ∀ t, γ t ∈ F
Path-connectedness within a subset
Informal description
Given a topological space $X$ and a subset $F \subseteq X$, two points $x, y \in X$ are said to be *joined in $F$* if there exists a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ such that $\gamma(t) \in F$ for all $t \in [0,1]$.
JoinedIn.mem theorem
(h : JoinedIn F x y) : x ∈ F ∧ y ∈ F
Full source 
theorem JoinedIn.mem (h : JoinedIn F x y) : x ∈ Fx ∈ F ∧ y ∈ F := by
  rcases h with ⟨γ, γ_in⟩
  have : γ 0 ∈ Fγ 0 ∈ F ∧ γ 1 ∈ F := by constructor <;> apply γ_in
  simpa using this
Path-connectedness in $F$ implies endpoints are in $F$
Informal description
Given a topological space $X$ and a subset $F \subseteq X$, if two points $x, y \in X$ are joined by a path in $F$ (i.e., there exists a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in F$ for all $t \in [0,1]$), then both $x$ and $y$ must belong to $F$.
JoinedIn.source_mem theorem
(h : JoinedIn F x y) : x ∈ F
Full source 
theorem JoinedIn.source_mem (h : JoinedIn F x y) : x ∈ F :=
  h.mem.1
Starting point of path-connected pair lies in subset
Informal description
Given a topological space $X$ and a subset $F \subseteq X$, if two points $x, y \in X$ are joined by a path in $F$ (i.e., there exists a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in F$ for all $t \in [0,1]$), then the starting point $x$ must belong to $F$.
JoinedIn.target_mem theorem
(h : JoinedIn F x y) : y ∈ F
Full source 
theorem JoinedIn.target_mem (h : JoinedIn F x y) : y ∈ F :=
  h.mem.2
Path-connectedness in $F$ implies target point is in $F$
Informal description
Given a topological space $X$ and a subset $F \subseteq X$, if two points $x, y \in X$ are joined by a path in $F$ (i.e., there exists a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in F$ for all $t \in [0,1]$), then the endpoint $y$ must belong to $F$.
JoinedIn.somePath definition
(h : JoinedIn F x y) : Path x y
Full source 
/-- When `x` and `y` are joined in `F`, choose a path from `x` to `y` inside `F` -/
def JoinedIn.somePath (h : JoinedIn F x y) : Path x y :=
  Classical.choose h
Path selection for points joined within a subset
Informal description
Given a topological space $X$, a subset $F \subseteq X$, and two points $x, y \in X$ that are joined in $F$ (i.e., there exists a continuous path from $x$ to $y$ lying entirely within $F$), the function selects such a path $\gamma: [0,1] \to X$ with $\gamma(0) = x$, $\gamma(1) = y$, and $\gamma(t) \in F$ for all $t \in [0,1]$.
JoinedIn.somePath_mem theorem
(h : JoinedIn F x y) (t : I) : h.somePath t ∈ F
Full source 
theorem JoinedIn.somePath_mem (h : JoinedIn F x y) (t : I) : h.somePath t ∈ F :=
  Classical.choose_spec h t
Path selected for joined points lies entirely within the subset
Informal description
Given a topological space $X$, a subset $F \subseteq X$, and two points $x, y \in X$ that are joined in $F$ (i.e., there exists a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in F$ for all $t \in [0,1]$), then for any $t \in [0,1]$, the point $\gamma(t)$ lies in $F$.
JoinedIn.joined_subtype theorem
(h : JoinedIn F x y) : Joined (⟨x, h.source_mem⟩ : F) (⟨y, h.target_mem⟩ : F)
Full source 
/-- If `x` and `y` are joined in the set `F`, then they are joined in the subtype `F`. -/
theorem JoinedIn.joined_subtype (h : JoinedIn F x y) :
    Joined (⟨x, h.source_mem⟩ : F) (⟨y, h.target_mem⟩ : F) :=
  ⟨{  toFun := fun t => ⟨h.somePath t, h.somePath_mem t⟩
      continuous_toFun := by fun_prop
      source' := by simp
      target' := by simp }⟩
Path-connectedness in subset implies path-connectedness in subtype
Informal description
Given a topological space $X$ and a subset $F \subseteq X$, if two points $x, y \in X$ are joined by a path in $F$ (i.e., there exists a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in F$ for all $t \in [0,1]$), then the corresponding points $\langle x, h.\text{source\_mem}\rangle$ and $\langle y, h.\text{target\_mem}\rangle$ in the subtype $F$ are joined by a path in $F$.
JoinedIn.ofLine theorem
{f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) (hF : f '' I ⊆ F) : JoinedIn F x y
Full source 
theorem JoinedIn.ofLine {f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y)
    (hF : f '' If '' I ⊆ F) : JoinedIn F x y :=
  ⟨Path.ofLine hf h₀ h₁, fun t => hF <| Path.ofLine_mem hf h₀ h₁ t⟩
Path-connectedness via continuous function restriction to unit interval
Informal description
Let $X$ be a topological space and $F \subseteq X$ a subset. Given a continuous function $f \colon \mathbb{R} \to X$ restricted to the unit interval $I = [0,1]$, with $f(0) = x$, $f(1) = y$, and the image $f(I) \subseteq F$, then $x$ and $y$ are joined in $F$ (i.e., there exists a continuous path from $x$ to $y$ lying entirely within $F$).
JoinedIn.joined theorem
(h : JoinedIn F x y) : Joined x y
Full source 
theorem JoinedIn.joined (h : JoinedIn F x y) : Joined x y :=
  ⟨h.somePath⟩
Path-connectedness in subset implies path-connectedness in whole space
Informal description
Given a topological space $X$, a subset $F \subseteq X$, and two points $x, y \in X$ that are joined in $F$ (i.e., there exists a continuous path from $x$ to $y$ lying entirely within $F$), then $x$ and $y$ are joined in the whole space $X$.
joinedIn_iff_joined theorem
(x_in : x ∈ F) (y_in : y ∈ F) : JoinedIn F x y ↔ Joined (⟨x, x_in⟩ : F) (⟨y, y_in⟩ : F)
Full source 
theorem joinedIn_iff_joined (x_in : x ∈ F) (y_in : y ∈ F) :
    JoinedInJoinedIn F x y ↔ Joined (⟨x, x_in⟩ : F) (⟨y, y_in⟩ : F) :=
  ⟨fun h => h.joined_subtype, fun h => ⟨h.somePath.map continuous_subtype_val, by simp⟩⟩
Equivalence of Path-Connectedness in Subset and Subtype
Informal description
For a topological space $X$ and a subset $F \subseteq X$, given two points $x, y \in F$, the following are equivalent: 1. There exists a continuous path from $x$ to $y$ lying entirely within $F$ (i.e., $x$ and $y$ are joined in $F$). 2. The corresponding points $\langle x, x\_in \rangle$ and $\langle y, y\_in \rangle$ in the subtype $F$ are joined by a path in $F$.
joinedIn_univ theorem
: JoinedIn univ x y ↔ Joined x y
Full source 
@[simp]
theorem joinedIn_univ : JoinedInJoinedIn univ x y ↔ Joined x y := by
  simp [JoinedIn, Joined, exists_true_iff_nonempty]
Equivalence of Path-Connectedness in Universal Set and Absolute Path-Connectedness
Informal description
For any two points $x$ and $y$ in a topological space $X$, the relation $\text{JoinedIn}(\text{univ}, x, y)$ holds if and only if $\text{Joined}(x, y)$ holds, where $\text{univ}$ denotes the universal set of $X$. In other words, $x$ and $y$ are joined by a path in the entire space $X$ if and only if they are joined by a path in $X$.
JoinedIn.mono theorem
{U V : Set X} (h : JoinedIn U x y) (hUV : U ⊆ V) : JoinedIn V x y
Full source 
theorem JoinedIn.mono {U V : Set X} (h : JoinedIn U x y) (hUV : U ⊆ V) : JoinedIn V x y :=
  ⟨h.somePath, fun t => hUV (h.somePath_mem t)⟩
Path-connectedness is monotonic with respect to subset inclusion
Informal description
Let $X$ be a topological space, and let $U, V \subseteq X$ be subsets with $U \subseteq V$. If two points $x, y \in X$ are joined by a path in $U$, then they are also joined by a path in $V$.
JoinedIn.refl theorem
(h : x ∈ F) : JoinedIn F x x
Full source 
theorem JoinedIn.refl (h : x ∈ F) : JoinedIn F x x :=
  ⟨Path.refl x, fun _t => h⟩
Reflexivity of Path-Connectedness within a Subset
Informal description
For any point $x$ in a subset $F$ of a topological space $X$, there exists a constant path from $x$ to itself that lies entirely within $F$. In other words, the relation "joined in $F$" is reflexive at $x$.
JoinedIn.symm theorem
(h : JoinedIn F x y) : JoinedIn F y x
Full source 
@[symm]
theorem JoinedIn.symm (h : JoinedIn F x y) : JoinedIn F y x := by
  obtain ⟨hx, hy⟩ := h.mem
  simp_all only [joinedIn_iff_joined]
  exact h.symm
Symmetry of Path-Connectedness within a Subset
Informal description
For any subset $F$ of a topological space $X$ and any two points $x, y \in X$, if there exists a continuous path from $x$ to $y$ lying entirely within $F$ (i.e., $\text{JoinedIn}(F, x, y)$ holds), then there also exists a continuous path from $y$ to $x$ lying entirely within $F$.
JoinedIn.trans theorem
(hxy : JoinedIn F x y) (hyz : JoinedIn F y z) : JoinedIn F x z
Full source 
theorem JoinedIn.trans (hxy : JoinedIn F x y) (hyz : JoinedIn F y z) : JoinedIn F x z := by
  obtain ⟨hx, hy⟩ := hxy.mem
  obtain ⟨hx, hy⟩ := hyz.mem
  simp_all only [joinedIn_iff_joined]
  exact hxy.trans hyz
Transitivity of Path-Connectedness within a Subset
Informal description
For any subset $F$ of a topological space $X$ and any three points $x, y, z \in X$, if there exists a continuous path from $x$ to $y$ lying entirely within $F$ and a continuous path from $y$ to $z$ lying entirely within $F$, then there exists a continuous path from $x$ to $z$ lying entirely within $F$.
Specializes.joinedIn theorem
(h : x ⤳ y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y
Full source 
theorem Specializes.joinedIn (h : x ⤳ y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y := by
  refine ⟨⟨⟨Set.piecewise {1} (const I y) (const I x), ?_⟩, by simp, by simp⟩, fun t ↦ ?_⟩
  · exact isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const
      fun _ ↦ h
  · simp only [Path.coe_mk_mk, piecewise]
    split_ifs <;> assumption
Path-connectedness of Specializing Points in a Subset
Informal description
Let $X$ be a topological space, $F \subseteq X$ a subset, and $x, y \in X$ such that $x$ specializes to $y$ (denoted $x \rightsquigarrow y$). If both $x$ and $y$ belong to $F$, then there exists a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in F$ for all $t \in [0,1]$.
Inseparable.joinedIn theorem
(h : Inseparable x y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y
Full source 
theorem Inseparable.joinedIn (h : Inseparable x y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y :=
  h.specializes.joinedIn hx hy
Path-connectedness of Inseparable Points in a Subset
Informal description
For any topological space $X$ and subset $F \subseteq X$, if two points $x, y \in X$ are inseparable (i.e., have identical neighborhood filters) and both belong to $F$, then there exists a continuous path from $x$ to $y$ lying entirely within $F$.
JoinedIn.map_continuousOn theorem
(h : JoinedIn F x y) {f : X → Y} (hf : ContinuousOn f F) : JoinedIn (f '' F) (f x) (f y)
Full source 
theorem JoinedIn.map_continuousOn (h : JoinedIn F x y) {f : X → Y} (hf : ContinuousOn f F) :
    JoinedIn (f '' F) (f x) (f y) :=
  let ⟨γ, hγ⟩ := h
  ⟨γ.map' <| hf.mono (range_subset_iff.mpr hγ), fun t ↦ mem_image_of_mem _ (hγ t)⟩
Continuous Image of Path-Connected Points is Path-Connected
Informal description
Let $X$ and $Y$ be topological spaces, $F \subseteq X$ a subset, and $x, y \in X$ two points joined by a path $\gamma$ in $F$ (i.e., $\gamma: [0,1] \to X$ is continuous with $\gamma(0) = x$, $\gamma(1) = y$, and $\gamma(t) \in F$ for all $t \in [0,1]$). If $f: X \to Y$ is continuous on $F$, then $f(x)$ and $f(y)$ are joined by a path in $f(F)$ (the image of $F$ under $f$).
JoinedIn.map theorem
(h : JoinedIn F x y) {f : X → Y} (hf : Continuous f) : JoinedIn (f '' F) (f x) (f y)
Full source 
theorem JoinedIn.map (h : JoinedIn F x y) {f : X → Y} (hf : Continuous f) :
    JoinedIn (f '' F) (f x) (f y) :=
  h.map_continuousOn hf.continuousOn
Continuous Image of Path-Connected Points is Path-Connected (Global Continuity Version)
Informal description
Let $X$ and $Y$ be topological spaces, $F \subseteq X$ a subset, and $x, y \in X$ two points joined by a path in $F$. If $f \colon X \to Y$ is continuous, then $f(x)$ and $f(y)$ are joined by a path in the image $f(F)$.
Topology.IsInducing.joinedIn_image theorem
{f : X → Y} (hf : IsInducing f) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y
Full source 
theorem Topology.IsInducing.joinedIn_image {f : X → Y} (hf : IsInducing f) (hx : x ∈ F)
    (hy : y ∈ F) : JoinedInJoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y := by
  refine ⟨?_, (.map · hf.continuous)⟩
  rintro ⟨γ, hγ⟩
  choose γ' hγ'F hγ' using hγ
  have h₀ : x ⤳ γ' 0 := by rw [← hf.specializes_iff, hγ', γ.source]
  have h₁ : γ' 1 ⤳ y := by rw [← hf.specializes_iff, hγ', γ.target]
  have h : JoinedIn F (γ' 0) (γ' 1) := by
    refine ⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩
    simpa only [hf.continuous_iff, comp_def, hγ'] using map_continuous γ
  exact (h₀.joinedIn hx (hγ'F _)).trans <| h.trans <| h₁.joinedIn (hγ'F _) hy
Path-Connectedness Preservation under Inducing Maps
Informal description
Let $X$ and $Y$ be topological spaces, $F \subseteq X$ a subset, and $f \colon X \to Y$ an inducing map. For any points $x, y \in F$, the images $f(x)$ and $f(y)$ are joined by a path in $f(F)$ if and only if $x$ and $y$ are joined by a path in $F$.
pathComponent definition
(x : X)
Full source 
/-- The path component of `x` is the set of points that can be joined to `x`. -/
def pathComponent (x : X) :=
  { y | Joined x y }
Path component of a point
Informal description
The path component of a point $x$ in a topological space $X$ is the set of all points $y \in X$ that can be connected to $x$ by a continuous path $\gamma : [0,1] \to X$ with $\gamma(0) = x$ and $\gamma(1) = y$.
mem_pathComponent_iff theorem
: x ∈ pathComponent y ↔ Joined y x
Full source 
theorem mem_pathComponent_iff : x ∈ pathComponent yx ∈ pathComponent y ↔ Joined y x := .rfl
Characterization of Path Component Membership via Path Connectivity
Informal description
For any two points $x$ and $y$ in a topological space $X$, the point $x$ belongs to the path component of $y$ if and only if there exists a continuous path from $y$ to $x$ in $X$.
mem_pathComponent_self theorem
(x : X) : x ∈ pathComponent x
Full source 
@[simp]
theorem mem_pathComponent_self (x : X) : x ∈ pathComponent x :=
  Joined.refl x
Reflexivity of Path Component Membership
Informal description
For any point $x$ in a topological space $X$, the point $x$ belongs to its own path component, i.e., $x \in \text{pathComponent}(x)$.
mem_pathComponent_of_mem theorem
(h : x ∈ pathComponent y) : y ∈ pathComponent x
Full source 
theorem mem_pathComponent_of_mem (h : x ∈ pathComponent y) : y ∈ pathComponent x :=
  Joined.symm h
Symmetry of Path Component Membership
Informal description
For any two points $x$ and $y$ in a topological space $X$, if $x$ belongs to the path component of $y$ (i.e., $x \in \text{pathComponent}(y)$), then $y$ also belongs to the path component of $x$ (i.e., $y \in \text{pathComponent}(x)$).
pathComponent_symm theorem
: x ∈ pathComponent y ↔ y ∈ pathComponent x
Full source 
theorem pathComponent_symm : x ∈ pathComponent yx ∈ pathComponent y ↔ y ∈ pathComponent x :=
  ⟨fun h => mem_pathComponent_of_mem h, fun h => mem_pathComponent_of_mem h⟩
Symmetry of Path Component Membership: $x \in \text{pathComponent}(y) \leftrightarrow y \in \text{pathComponent}(x)$
Informal description
For any two points $x$ and $y$ in a topological space $X$, the point $x$ belongs to the path component of $y$ if and only if $y$ belongs to the path component of $x$. In other words, $x \in \text{pathComponent}(y) \leftrightarrow y \in \text{pathComponent}(x)$.
pathComponent_congr theorem
(h : x ∈ pathComponent y) : pathComponent x = pathComponent y
Full source 
theorem pathComponent_congr (h : x ∈ pathComponent y) : pathComponent x = pathComponent y := by
  ext z
  constructor
  · intro h'
    rw [pathComponent_symm]
    exact (h.trans h').symm
  · intro h'
    rw [pathComponent_symm] at h' ⊢
    exact h'.trans h
Path Components Coincide for Connected Points
Informal description
For any two points $x$ and $y$ in a topological space $X$, if $x$ belongs to the path component of $y$, then the path component of $x$ equals the path component of $y$. In other words, $x \in \text{pathComponent}(y)$ implies $\text{pathComponent}(x) = \text{pathComponent}(y)$.
pathComponent_subset_component theorem
(x : X) : pathComponent x ⊆ connectedComponent x
Full source 
theorem pathComponent_subset_component (x : X) : pathComponentpathComponent x ⊆ connectedComponent x :=
  fun y h =>
  (isConnected_range h.somePath.continuous).subset_connectedComponent ⟨0, by simp⟩ ⟨1, by simp⟩
Path Component is Subset of Connected Component
Informal description
For any point $x$ in a topological space $X$, the path component of $x$ is a subset of the connected component of $x$. That is, every point that can be connected to $x$ by a continuous path is also in the same connected component as $x$.
pathComponentIn definition
(x : X) (F : Set X)
Full source 
/-- The path component of `x` in `F` is the set of points that can be joined to `x` in `F`. -/
def pathComponentIn (x : X) (F : Set X) :=
  { y | JoinedIn F x y }
Path component within a subset
Informal description
Given a topological space $X$, a subset $F \subseteq X$, and a point $x \in X$, the *path component of $x$ in $F$* is the set of all points $y \in X$ that can be joined to $x$ by a continuous path $\gamma: [0,1] \to X$ with $\gamma(t) \in F$ for all $t \in [0,1]$.
pathComponentIn_univ theorem
(x : X) : pathComponentIn x univ = pathComponent x
Full source 
@[simp]
theorem pathComponentIn_univ (x : X) : pathComponentIn x univ = pathComponent x := by
  simp [pathComponentIn, pathComponent, JoinedIn, Joined, exists_true_iff_nonempty]
Equality of Path Components in Universal Set and Full Space
Informal description
For any point $x$ in a topological space $X$, the path component of $x$ within the universal set $\mathrm{univ} = X$ is equal to the path component of $x$ in $X$. That is, $\mathrm{pathComponentIn}\, x\, X = \mathrm{pathComponent}\, x$.
Joined.mem_pathComponent theorem
(hyz : Joined y z) (hxy : y ∈ pathComponent x) : z ∈ pathComponent x
Full source 
theorem Joined.mem_pathComponent (hyz : Joined y z) (hxy : y ∈ pathComponent x) :
    z ∈ pathComponent x :=
  hxy.trans hyz
Path Component Membership under Path Joining
Informal description
For any points $x, y, z$ in a topological space $X$, if $y$ is joined to $z$ by a path and $y$ belongs to the path component of $x$, then $z$ also belongs to the path component of $x$.
mem_pathComponentIn_self theorem
(h : x ∈ F) : x ∈ pathComponentIn x F
Full source 
theorem mem_pathComponentIn_self (h : x ∈ F) : x ∈ pathComponentIn x F :=
  JoinedIn.refl h
Self-Membership in Path Component Within a Subset
Informal description
For any point $x$ in a subset $F$ of a topological space $X$, the point $x$ belongs to its own path component within $F$, i.e., $x \in \text{pathComponentIn}_F(x)$.
pathComponentIn_subset theorem
: pathComponentIn x F ⊆ F
Full source 
theorem pathComponentIn_subset : pathComponentInpathComponentIn x F ⊆ F :=
  fun _ hy ↦ hy.target_mem
Path Component Within Subset is Contained in Subset
Informal description
For any topological space $X$, subset $F \subseteq X$, and point $x \in X$, the path component of $x$ in $F$ is a subset of $F$. In other words, every point $y$ that can be connected to $x$ by a path lying entirely in $F$ must belong to $F$.
pathComponentIn_nonempty_iff theorem
: (pathComponentIn x F).Nonempty ↔ x ∈ F
Full source 
theorem pathComponentIn_nonempty_iff : (pathComponentIn x F).Nonempty ↔ x ∈ F :=
  ⟨fun ⟨_, ⟨γ, hγ⟩⟩ ↦ γ.source ▸ hγ 0, fun hx ↦ ⟨x, mem_pathComponentIn_self hx⟩⟩
Nonemptiness of Path Component in Subset Equivalent to Membership
Informal description
For any topological space $X$, subset $F \subseteq X$, and point $x \in X$, the path component of $x$ in $F$ is nonempty if and only if $x$ belongs to $F$.
pathComponentIn_congr theorem
(h : x ∈ pathComponentIn y F) : pathComponentIn x F = pathComponentIn y F
Full source 
theorem pathComponentIn_congr (h : x ∈ pathComponentIn y F) :
    pathComponentIn x F = pathComponentIn y F := by
  ext; exact ⟨h.trans, h.symm.trans⟩
Equality of Path Components for Points in the Same Path Component
Informal description
For any topological space $X$, subset $F \subseteq X$, and points $x, y \in X$, if $x$ belongs to the path component of $y$ in $F$, then the path component of $x$ in $F$ equals the path component of $y$ in $F$.
pathComponentIn_mono theorem
{G : Set X} (h : F ⊆ G) : pathComponentIn x F ⊆ pathComponentIn x G
Full source 
@[gcongr]
theorem pathComponentIn_mono {G : Set X} (h : F ⊆ G) :
    pathComponentInpathComponentIn x F ⊆ pathComponentIn x G :=
  fun _ ⟨γ, hγ⟩ ↦ ⟨γ, fun t ↦ h (hγ t)⟩
Monotonicity of Path Components with Respect to Subset Inclusion
Informal description
For any topological space $X$, subsets $F, G \subseteq X$ with $F \subseteq G$, and point $x \in X$, the path component of $x$ in $F$ is contained in the path component of $x$ in $G$. In other words, if $F \subseteq G$, then $\text{pathComponentIn}(x, F) \subseteq \text{pathComponentIn}(x, G)$.
IsPathConnected definition
(F : Set X) : Prop
Full source 
/-- A set `F` is path connected if it contains a point that can be joined to all other in `F`. -/
def IsPathConnected (F : Set X) : Prop :=
  ∃ x ∈ F, ∀ {y}, y ∈ F → JoinedIn F x y
Path-connected subset of a topological space
Informal description
A subset $F$ of a topological space $X$ is called *path connected* if there exists a point $x \in F$ such that for every $y \in F$, there is a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in F$ for all $t \in [0,1]$.
isPathConnected_iff_eq theorem
: IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn x F = F
Full source 
theorem isPathConnected_iff_eq : IsPathConnectedIsPathConnected F ↔ ∃ x ∈ F, pathComponentIn x F = F := by
  constructor <;> rintro ⟨x, x_in, h⟩ <;> use x, x_in
  · ext y
    exact ⟨fun hy => hy.mem.2, h⟩
  · intro y y_in
    rwa [← h] at y_in
Path-Connectedness Criterion: $F$ is path-connected $\iff$ $\exists x \in F, \text{pathComponentIn}(x, F) = F$
Informal description
A subset $F$ of a topological space $X$ is path-connected if and only if there exists a point $x \in F$ such that the path component of $x$ in $F$ equals $F$ itself.
IsPathConnected.joinedIn theorem
(h : IsPathConnected F) : ∀ᵉ (x ∈ F) (y ∈ F), JoinedIn F x y
Full source 
theorem IsPathConnected.joinedIn (h : IsPathConnected F) :
    ∀ᵉ (x ∈ F) (y ∈ F), JoinedIn F x y := fun _x x_in _y y_in =>
  let ⟨_b, _b_in, hb⟩ := h
  (hb x_in).symm.trans (hb y_in)
Path-connectedness implies any two points are joined by a path in $F$
Informal description
If $F$ is a path-connected subset of a topological space $X$, then for any two points $x, y \in F$, there exists a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in F$ for all $t \in [0,1]$.
isPathConnected_iff theorem
: IsPathConnected F ↔ F.Nonempty ∧ ∀ᵉ (x ∈ F) (y ∈ F), JoinedIn F x y
Full source 
theorem isPathConnected_iff :
    IsPathConnectedIsPathConnected F ↔ F.Nonempty ∧ ∀ᵉ (x ∈ F) (y ∈ F), JoinedIn F x y :=
  ⟨fun h =>
    ⟨let ⟨b, b_in, _hb⟩ := h; ⟨b, b_in⟩, h.joinedIn⟩,
    fun ⟨⟨b, b_in⟩, h⟩ => ⟨b, b_in, fun x_in => h _ b_in _ x_in⟩⟩
Characterization of Path-Connected Subsets: $F$ path-connected $\iff$ $F$ nonempty and any two points in $F$ are joined by a path in $F$
Informal description
A subset $F$ of a topological space $X$ is path-connected if and only if $F$ is nonempty and for any two points $x, y \in F$, there exists a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in F$ for all $t \in [0,1]$.
IsPathConnected.image' theorem
(hF : IsPathConnected F) {f : X → Y} (hf : ContinuousOn f F) : IsPathConnected (f '' F)
Full source 
/-- If `f` is continuous on `F` and `F` is path-connected, so is `f(F)`. -/
theorem IsPathConnected.image' (hF : IsPathConnected F)
    {f : X → Y} (hf : ContinuousOn f F) : IsPathConnected (f '' F) := by
  rcases hF with ⟨x, x_in, hx⟩
  use f x, mem_image_of_mem f x_in
  rintro _ ⟨y, y_in, rfl⟩
  refine ⟨(hx y_in).somePath.map' ?_, fun t ↦ ⟨_, (hx y_in).somePath_mem t, rfl⟩⟩
  exact hf.mono (range_subset_iff.2 (hx y_in).somePath_mem)
Continuous Image of Path-Connected Set is Path-Connected
Informal description
Let $X$ and $Y$ be topological spaces, $F \subseteq X$ a path-connected subset, and $f: X \to Y$ a function continuous on $F$. Then the image $f(F)$ is path-connected in $Y$.
IsPathConnected.image theorem
(hF : IsPathConnected F) {f : X → Y} (hf : Continuous f) : IsPathConnected (f '' F)
Full source 
/-- If `f` is continuous and `F` is path-connected, so is `f(F)`. -/
theorem IsPathConnected.image (hF : IsPathConnected F) {f : X → Y} (hf : Continuous f) :
    IsPathConnected (f '' F) :=
  hF.image' hf.continuousOn
Continuous Image of Path-Connected Set is Path-Connected
Informal description
Let $X$ and $Y$ be topological spaces, $F \subseteq X$ a path-connected subset, and $f \colon X \to Y$ a continuous function. Then the image $f(F)$ is path-connected in $Y$.
Topology.IsInducing.isPathConnected_iff theorem
{f : X → Y} (hf : IsInducing f) : IsPathConnected F ↔ IsPathConnected (f '' F)
Full source 
/-- If `f : X → Y` is an inducing map, `f(F)` is path-connected iff `F` is. -/
nonrec theorem Topology.IsInducing.isPathConnected_iff {f : X → Y} (hf : IsInducing f) :
    IsPathConnectedIsPathConnected F ↔ IsPathConnected (f '' F) := by
  simp only [IsPathConnected, forall_mem_image, exists_mem_image]
  refine exists_congr fun x ↦ and_congr_right fun hx ↦ forall₂_congr fun y hy ↦ ?_
  rw [hf.joinedIn_image hx hy]
Path-Connectedness is Preserved Under Inducing Maps: $F$ is path-connected $\leftrightarrow$ $f(F)$ is path-connected
Informal description
Let $X$ and $Y$ be topological spaces, $F \subseteq X$ a subset, and $f \colon X \to Y$ an inducing map. Then $F$ is path-connected if and only if its image $f(F)$ is path-connected.
Homeomorph.isPathConnected_image theorem
{s : Set X} (h : X ≃ₜ Y) : IsPathConnected (h '' s) ↔ IsPathConnected s
Full source 
/-- If `h : X → Y` is a homeomorphism, `h(s)` is path-connected iff `s` is. -/
@[simp]
theorem Homeomorph.isPathConnected_image {s : Set X} (h : X ≃ₜ Y) :
    IsPathConnectedIsPathConnected (h '' s) ↔ IsPathConnected s :=
  h.isInducing.isPathConnected_iff.symm
Path-connectedness is preserved under homeomorphism: $h(s)$ is path-connected $\leftrightarrow$ $s$ is path-connected
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, and $h \colon X \simeq_{\text{top}} Y$ a homeomorphism. Then the image $h(s)$ is path-connected if and only if $s$ is path-connected.
Homeomorph.isPathConnected_preimage theorem
{s : Set Y} (h : X ≃ₜ Y) : IsPathConnected (h ⁻¹' s) ↔ IsPathConnected s
Full source 
/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is path-connected iff `s` is. -/
@[simp]
theorem Homeomorph.isPathConnected_preimage {s : Set Y} (h : X ≃ₜ Y) :
    IsPathConnectedIsPathConnected (h ⁻¹' s) ↔ IsPathConnected s := by
  rw [← Homeomorph.image_symm]; exact h.symm.isPathConnected_image
Path-connectedness of preimage under homeomorphism: $h^{-1}(s)$ is path-connected $\leftrightarrow$ $s$ is path-connected
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq Y$ a subset, and $h \colon X \simeq_{\text{top}} Y$ a homeomorphism. Then the preimage $h^{-1}(s)$ is path-connected if and only if $s$ is path-connected.
IsPathConnected.mem_pathComponent theorem
(h : IsPathConnected F) (x_in : x ∈ F) (y_in : y ∈ F) : y ∈ pathComponent x
Full source 
theorem IsPathConnected.mem_pathComponent (h : IsPathConnected F) (x_in : x ∈ F) (y_in : y ∈ F) :
    y ∈ pathComponent x :=
  (h.joinedIn x x_in y y_in).joined
Path-connected subset implies membership in path component
Informal description
Let $F$ be a path-connected subset of a topological space $X$, and let $x, y \in F$. Then $y$ belongs to the path component of $x$ in $X$, i.e., $y \in \text{pathComponent}(x)$.
IsPathConnected.subset_pathComponent theorem
(h : IsPathConnected F) (x_in : x ∈ F) : F ⊆ pathComponent x
Full source 
theorem IsPathConnected.subset_pathComponent (h : IsPathConnected F) (x_in : x ∈ F) :
    F ⊆ pathComponent x := fun _y y_in => h.mem_pathComponent x_in y_in
Path-connected subset is contained in path component
Informal description
Let $F$ be a path-connected subset of a topological space $X$, and let $x \in F$. Then $F$ is contained in the path component of $x$, i.e., $F \subseteq \text{pathComponent}(x)$.
IsPathConnected.subset_pathComponentIn theorem
{s : Set X} (hs : IsPathConnected s) (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ pathComponentIn x F
Full source 
theorem IsPathConnected.subset_pathComponentIn {s : Set X} (hs : IsPathConnected s)
    (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ pathComponentIn x F :=
  fun y hys ↦ (hs.joinedIn x hxs y hys).mono hsF
Path-connected subset is contained in path component within a superset
Informal description
Let $X$ be a topological space, $F \subseteq X$ a subset, and $s \subseteq X$ a path-connected subset containing $x \in s$. If $s \subseteq F$, then every point in $s$ is in the path component of $x$ within $F$, i.e., $s \subseteq \text{pathComponentIn}_F(x)$.
isPathConnected_pathComponentIn theorem
(h : x ∈ F) : IsPathConnected (pathComponentIn x F)
Full source 
theorem isPathConnected_pathComponentIn (h : x ∈ F) : IsPathConnected (pathComponentIn x F) :=
  ⟨x, mem_pathComponentIn_self h, fun ⟨γ, hγ⟩ ↦ by
    refine ⟨γ, fun t ↦
      ⟨(γ.truncateOfLE t.2.1).cast (γ.extend_zero.symm) (γ.extend_extends' t).symm, fun t' ↦ ?_⟩⟩
    dsimp [Path.truncateOfLE, Path.truncate]
    exact γ.extend_extends' ⟨min (max t'.1 0) t.1, by simp [t.2.1, t.2.2]⟩ ▸ hγ _⟩
Path-connectedness of path components within a subset
Informal description
For any topological space $X$, subset $F \subseteq X$, and point $x \in F$, the path component of $x$ in $F$ (i.e., the set of all points in $X$ that can be connected to $x$ by a path lying entirely in $F$) is path-connected.
IsPathConnected.union theorem
{U V : Set X} (hU : IsPathConnected U) (hV : IsPathConnected V) (hUV : (U ∩ V).Nonempty) : IsPathConnected (U ∪ V)
Full source 
theorem IsPathConnected.union {U V : Set X} (hU : IsPathConnected U) (hV : IsPathConnected V)
    (hUV : (U ∩ V).Nonempty) : IsPathConnected (U ∪ V) := by
  rcases hUV with ⟨x, xU, xV⟩
  use x, Or.inl xU
  rintro y (yU | yV)
  · exact (hU.joinedIn x xU y yU).mono subset_union_left
  · exact (hV.joinedIn x xV y yV).mono subset_union_right
Union of Path-Connected Sets with Nonempty Intersection is Path-Connected
Informal description
Let $X$ be a topological space and $U, V \subseteq X$ be two path-connected subsets such that $U \cap V$ is nonempty. Then the union $U \cup V$ is also path-connected.
IsPathConnected.preimage_coe theorem
{U W : Set X} (hW : IsPathConnected W) (hWU : W ⊆ U) : IsPathConnected (((↑) : U → X) ⁻¹' W)
Full source 
/-- 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.preimage_coe {U W : Set X} (hW : IsPathConnected W) (hWU : W ⊆ U) :
    IsPathConnected (((↑) : U → X) ⁻¹' W) := by
  rwa [IsInducing.subtypeVal.isPathConnected_iff, Subtype.image_preimage_val, inter_eq_right.2 hWU]
Path-connectedness of Preimage under Inclusion Map
Informal description
Let $X$ be a topological space, $U, W \subseteq X$ with $W \subseteq U$, and suppose $W$ is path-connected. Then the preimage of $W$ under the inclusion map $\iota: U \to X$ is path-connected in the subspace topology of $U$.
IsPathConnected.exists_path_through_family theorem
{n : ℕ} {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1) → X) (hp : ∀ i, p i ∈ s) : ∃ γ : Path (p 0) (p n), range γ ⊆ s ∧ ∀ i, p i ∈ range γ
Full source 
theorem IsPathConnected.exists_path_through_family {n : ℕ}
    {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1) → X) (hp : ∀ i, p i ∈ s) :
    ∃ γ : Path (p 0) (p n), range γ ⊆ s ∧ ∀ i, p i ∈ range γ := by
  let p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, n.zero_lt_succ⟩
  obtain ⟨γ, hγ⟩ : ∃ γ : Path (p' 0) (p' n), (∀ i ≤ n, p' i ∈ range γ) ∧ range γ ⊆ s := by
    have hp' : ∀ i ≤ n, p' i ∈ s := by
      intro i hi
      simp [p', Nat.lt_succ_of_le hi, hp]
    clear_value p'
    clear hp p
    induction n with
    | zero =>
      use Path.refl (p' 0)
      constructor
      · rintro i hi
        rw [Nat.le_zero.mp hi]
        exact ⟨0, rfl⟩
      · rw [range_subset_iff]
        rintro _x
        exact hp' 0 le_rfl
    | succ n hn =>
      rcases hn fun i hi => hp' i <| Nat.le_succ_of_le hi with ⟨γ₀, hγ₀⟩
      rcases h.joinedIn (p' n) (hp' n n.le_succ) (p' <| n + 1) (hp' (n + 1) <| le_rfl) with
        ⟨γ₁, hγ₁⟩
      let γ : Path (p' 0) (p' <| n + 1) := γ₀.trans γ₁
      use γ
      have range_eq : range γ = rangerange γ₀ ∪ range γ₁ := γ₀.trans_range γ₁
      constructor
      · rintro i hi
        by_cases hi' : i ≤ n
        · rw [range_eq]
          left
          exact hγ₀.1 i hi'
        · rw [not_le, ← Nat.succ_le_iff] at hi'
          have : i = n.succ := le_antisymm hi hi'
          rw [this]
          use 1
          exact γ.target
      · rw [range_eq]
        apply union_subset hγ₀.2
        rw [range_subset_iff]
        exact hγ₁
  have hpp' : ∀ k < n + 1, p k = p' k := by
    intro k hk
    simp only [p', hk, dif_pos]
    congr
    ext
    rw [Fin.val_cast_of_lt hk]
  use γ.cast (hpp' 0 n.zero_lt_succ) (hpp' n n.lt_succ_self)
  simp only [γ.cast_coe]
  refine And.intro hγ.2 ?_
  rintro ⟨i, hi⟩
  suffices p ⟨i, hi⟩ = p' i by convert hγ.1 i (Nat.le_of_lt_succ hi)
  rw [← hpp' i hi]
  suffices i = i % n.succ by congr
  rw [Nat.mod_eq_of_lt hi]
Existence of Path Through Finite Sequence in Path-Connected Set
Informal description
Let $X$ be a topological space and $s \subseteq X$ a path-connected subset. For any finite sequence of points $p_0, p_1, \ldots, p_n$ in $s$ (where $n$ is a natural number), there exists a continuous path $\gamma: [0,1] \to X$ from $p_0$ to $p_n$ such that: 1. The image of $\gamma$ is contained in $s$ (i.e., $\gamma(t) \in s$ for all $t \in [0,1]$), and 2. Every point $p_i$ in the sequence lies in the image of $\gamma$.
IsPathConnected.exists_path_through_family' theorem
{n : ℕ} {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1) → X) (hp : ∀ i, p i ∈ s) : ∃ (γ : Path (p 0) (p n)) (t : Fin (n + 1) → I), (∀ t, γ t ∈ s) ∧ ∀ i, γ (t i) = p i
Full source 
theorem IsPathConnected.exists_path_through_family' {n : ℕ}
    {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1) → X) (hp : ∀ i, p i ∈ s) :
    ∃ (γ : Path (p 0) (p n)) (t : Fin (n + 1) → I), (∀ t, γ t ∈ s) ∧ ∀ i, γ (t i) = p i := by
  rcases h.exists_path_through_family p hp with ⟨γ, hγ⟩
  rcases hγ with ⟨h₁, h₂⟩
  simp only [range, mem_setOf_eq] at h₂
  rw [range_subset_iff] at h₁
  choose! t ht using h₂
  exact ⟨γ, t, h₁, ht⟩
Existence of Parameterized Path Through Finite Sequence in Path-Connected Set
Informal description
Let $X$ be a topological space and $s \subseteq X$ a path-connected subset. For any finite sequence of points $p_0, p_1, \ldots, p_n$ in $s$ (where $n$ is a natural number), there exists a continuous path $\gamma: [0,1] \to X$ from $p_0$ to $p_n$ and a sequence of parameters $t_0, t_1, \ldots, t_n \in [0,1]$ such that: 1. The image of $\gamma$ is contained in $s$ (i.e., $\gamma(t) \in s$ for all $t \in [0,1]$), and 2. For each $i$, $\gamma(t_i) = p_i$.
PathConnectedSpace structure
(X : Type*) [TopologicalSpace X]
Full source 
/-- A topological space is path-connected if it is non-empty and every two points can be
joined by a continuous path. -/
@[mk_iff]
class PathConnectedSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- A path-connected space must be nonempty. -/
  nonempty : Nonempty X
  /-- Any two points in a path-connected space must be joined by a continuous path. -/
  joined : ∀ x y : X, Joined x y
Path-connected space
Informal description
A topological space $X$ is called path-connected if it is non-empty and for any two points $x, y \in X$, there exists a continuous path from $x$ to $y$.
pathConnectedSpace_iff_zerothHomotopy theorem
: PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
Full source 
theorem pathConnectedSpace_iff_zerothHomotopy :
    PathConnectedSpacePathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) := by
  letI := pathSetoid X
  constructor
  · intro h
    refine ⟨(nonempty_quotient_iff _).mpr h.1, ⟨?_⟩⟩
    rintro ⟨x⟩ ⟨y⟩
    exact Quotient.sound (PathConnectedSpace.joined x y)
  · unfold ZerothHomotopy
    rintro ⟨h, h'⟩
    exact ⟨(nonempty_quotient_iff _).mp h, fun x y => Quotient.exact <| Subsingleton.elim ⟦x⟧ ⟦y⟧⟩
Path-connectedness Criterion via Zeroth Homotopy
Informal description
A topological space $X$ is path-connected if and only if its zeroth homotopy (the set of path-connected components) is non-empty and has exactly one element.
PathConnectedSpace.somePath definition
(x y : X) : Path x y
Full source 
/-- Use path-connectedness to build a path between two points. -/
def somePath (x y : X) : Path x y :=
  Nonempty.some (joined x y)
Path selection in a path-connected space
Informal description
Given a path-connected space $X$ and two points $x, y \in X$, the function `PathConnectedSpace.somePath` selects some continuous path from $x$ to $y$.
pathConnectedSpace_iff_univ theorem
: PathConnectedSpace X ↔ IsPathConnected (univ : Set X)
Full source 
theorem pathConnectedSpace_iff_univ : PathConnectedSpacePathConnectedSpace X ↔ IsPathConnected (univ : Set X) := by
  simp [pathConnectedSpace_iff, isPathConnected_iff, nonempty_iff_univ_nonempty]
Path-connectedness Criterion via Universal Set
Informal description
A topological space $X$ is path-connected if and only if the universal set $\text{univ} = X$ is path-connected. That is, $X$ is path-connected precisely when there exists a point $x \in X$ such that for every $y \in X$, there is a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in X$ for all $t \in [0,1]$.
isPathConnected_iff_pathConnectedSpace theorem
: IsPathConnected F ↔ PathConnectedSpace F
Full source 
theorem isPathConnected_iff_pathConnectedSpace : IsPathConnectedIsPathConnected F ↔ PathConnectedSpace F := by
  rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ,
    Subtype.range_val_subtype, setOf_mem_eq]
Path-connectedness of Subset vs. Subspace: $F$ is path-connected $\leftrightarrow$ $F$ is a path-connected space
Informal description
A subset $F$ of a topological space $X$ is path-connected if and only if the subspace $F$ (equipped with the subspace topology) is a path-connected space.
isPathConnected_univ theorem
[PathConnectedSpace X] : IsPathConnected (univ : Set X)
Full source 
theorem isPathConnected_univ [PathConnectedSpace X] : IsPathConnected (univ : Set X) :=
  pathConnectedSpace_iff_univ.mp inferInstance
Path-connectedness of Universal Set in Path-connected Space
Informal description
If $X$ is a path-connected topological space, then the universal set $\text{univ} = X$ is path-connected. That is, there exists a point $x \in X$ such that for every $y \in X$, there is a continuous path $\gamma: [0,1] \to X$ from $x$ to $y$ with $\gamma(t) \in X$ for all $t \in [0,1]$.
isPathConnected_range theorem
[PathConnectedSpace X] {f : X → Y} (hf : Continuous f) : IsPathConnected (range f)
Full source 
theorem isPathConnected_range [PathConnectedSpace X] {f : X → Y} (hf : Continuous f) :
    IsPathConnected (range f) := by
  rw [← image_univ]
  exact isPathConnected_univ.image hf
Range of Continuous Function from Path-Connected Space is Path-Connected
Informal description
Let $X$ be a path-connected topological space and $f \colon X \to Y$ a continuous function. Then the range of $f$ is path-connected in $Y$.
Function.Surjective.pathConnectedSpace theorem
[PathConnectedSpace X] {f : X → Y} (hf : Surjective f) (hf' : Continuous f) : PathConnectedSpace Y
Full source 
theorem Function.Surjective.pathConnectedSpace [PathConnectedSpace X]
    {f : X → Y} (hf : Surjective f) (hf' : Continuous f) : PathConnectedSpace Y := by
  rw [pathConnectedSpace_iff_univ, ← hf.range_eq]
  exact isPathConnected_range hf'
Continuous Surjective Image of Path-Connected Space is Path-Connected
Informal description
Let $X$ be a path-connected topological space and $f \colon X \to Y$ a continuous surjective function. Then $Y$ is also path-connected.
Real.instPathConnectedSpace instance
: PathConnectedSpace ℝ
Full source 
/-- This is a special case of `NormedSpace.instPathConnectedSpace` (and
`IsTopologicalAddGroup.pathConnectedSpace`). It exists only to simplify dependencies. -/
instance Real.instPathConnectedSpace : PathConnectedSpace ℝ where
  joined x y := ⟨⟨⟨fun (t : I) ↦ (1 - t) * x + t * y, by fun_prop⟩, by simp, by simp⟩⟩
  nonempty := inferInstance
Path-Connectedness of the Real Numbers
Informal description
The real numbers $\mathbb{R}$ form a path-connected space, meaning that for any two points $x, y \in \mathbb{R}$, there exists a continuous path from $x$ to $y$.
pathConnectedSpace_iff_eq theorem
: PathConnectedSpace X ↔ ∃ x : X, pathComponent x = univ
Full source 
theorem pathConnectedSpace_iff_eq : PathConnectedSpacePathConnectedSpace X ↔ ∃ x : X, pathComponent x = univ := by
  simp [pathConnectedSpace_iff_univ, isPathConnected_iff_eq]
Characterization of Path-Connected Spaces via Path Components
Informal description
A topological space $X$ is path-connected if and only if there exists a point $x \in X$ such that the path component of $x$ equals the entire space $X$, i.e., $\mathrm{pathComponent}(x) = X$.
PathConnectedSpace.connectedSpace instance
[PathConnectedSpace X] : ConnectedSpace X
Full source 
instance (priority := 100) PathConnectedSpace.connectedSpace [PathConnectedSpace X] :
    ConnectedSpace X := by
  rw [connectedSpace_iff_connectedComponent]
  rcases isPathConnected_iff_eq.mp (pathConnectedSpace_iff_univ.mp ‹_›) with ⟨x, _x_in, hx⟩
  use x
  rw [← univ_subset_iff]
  exact (by simpa using hx : pathComponent x = univ) ▸ pathComponent_subset_component x
Path-Connected Implies Connected
Informal description
Every path-connected topological space $X$ is also connected.
PathConnectedSpace.exists_path_through_family theorem
{n : ℕ} (p : Fin (n + 1) → X) : ∃ γ : Path (p 0) (p n), ∀ i, p i ∈ range γ
Full source 
theorem exists_path_through_family {n : ℕ} (p : Fin (n + 1) → X) :
    ∃ γ : Path (p 0) (p n), ∀ i, p i ∈ range γ := by
  have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)
  rcases this.exists_path_through_family p fun _i => True.intro with ⟨γ, -, h⟩
  exact ⟨γ, h⟩
Existence of Path Through Finite Sequence in Path-Connected Space
Informal description
Let $X$ be a path-connected topological space. For any finite sequence of points $p_0, p_1, \ldots, p_n$ in $X$ (where $n$ is a natural number), there exists a continuous path $\gamma: [0,1] \to X$ from $p_0$ to $p_n$ such that every point $p_i$ in the sequence lies in the image of $\gamma$.
PathConnectedSpace.exists_path_through_family' theorem
{n : ℕ} (p : Fin (n + 1) → X) : ∃ (γ : Path (p 0) (p n)) (t : Fin (n + 1) → I), ∀ i, γ (t i) = p i
Full source 
theorem exists_path_through_family' {n : ℕ} (p : Fin (n + 1) → X) :
    ∃ (γ : Path (p 0) (p n)) (t : Fin (n + 1) → I), ∀ i, γ (t i) = p i := by
  have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)
  rcases this.exists_path_through_family' p fun _i => True.intro with ⟨γ, t, -, h⟩
  exact ⟨γ, t, h⟩
Existence of Parameterized Path Through Finite Sequence in Path-Connected Space
Informal description
Let $X$ be a path-connected topological space. For any finite sequence of points $p_0, p_1, \ldots, p_n$ in $X$ (where $n$ is a natural number), there exists a continuous path $\gamma: [0,1] \to X$ from $p_0$ to $p_n$ and a sequence of parameters $t_0, t_1, \ldots, t_n \in [0,1]$ such that $\gamma(t_i) = p_i$ for each $i$.