Path connectedness

Main definitions

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

• Path (x y : X) is the type of paths from x to y, i.e., continuous maps from I to X mapping 0 to x and 1 to y.
• Path.map is the image of a path under a continuous map.
• 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.
• LocPathConnectedSpace X is a predicate class asserting that X is locally path-connected: each point has a basis of path-connected neighborhoods (we do not ask these to be open).

## Main theorems

• Joined and JoinedIn F are transitive relations.

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

For locally path connected spaces, we have

• pathConnectedSpace_iff_connectedSpace : PathConnectedSpace X ↔ ConnectedSpace X
• IsOpen.isConnected_iff_isPathConnected (U_op : IsOpen U) : IsPathConnected U ↔ IsConnected U

Implementation notes

By default, all paths have I as their source and X as their target, but there is an operation Set.IccExtend that will extend any continuous map γ : I → X into a continuous map IccExtend zero_le_one γ : ℝ → X that is constant before 0 and after 1.

This is used to define Path.extend that turns γ : Path x y into a continuous map γ.extend : ℝ → X whose restriction to I is the original γ, and is equal to x on (-∞, 0] and to y on [1, +∞).

Paths

structure Path {X : Type u_1} [TopologicalSpace X] (x : X) (y : X) extends ContinuousMap : Type u_1

Continuous path connecting two points x and y in a topological space

• toFun : ↑unitInterval → X
• continuous_toFun : Continuous self.toFun
• source' : self.toFun 0 = x

  The start point of a Path.

• target' : self.toFun 1 = y

  The end point of a Path.

instance Path.funLike {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} : FunLike (Path x y) (↑unitInterval) X

Equations

• Path.funLike = { coe := fun (γ : Path x y) => ⇑γ.toContinuousMap, coe_injective' := ⋯ }

instance Path.continuousMapClass {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} : ContinuousMapClass (Path x y) (↑unitInterval) X

Equations

• ⋯ = ⋯

theorem Path.ext {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {γ₁ : Path x y} {γ₂ : Path x y} : ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂

@[simp]

theorem Path.coe_mk_mk {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (f : ↑unitInterval → X) (h₁ : Continuous f) (h₂ : f 0 = x) (h₃ : f 1 = y) : ⇑{ toContinuousMap := { toFun := f, continuous_toFun := h₁ }, source' := h₂, target' := h₃ } = f

theorem Path.continuous {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Continuous ⇑γ

@[simp]

theorem Path.source {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : γ 0 = x

@[simp]

theorem Path.target {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : γ 1 = y

def Path.simps.apply {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : ↑unitInterval → X

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

• Path.simps.apply γ = ⇑γ

@[simp]

theorem Path.coe_toContinuousMap {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : ⇑γ.toContinuousMap = ⇑γ

@[simp]

theorem Path.coe_mk {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : ⇑↑γ = ⇑γ

instance Path.hasUncurryPath {X : Type u_4} {α : Type u_5} [TopologicalSpace X] {x : α → X} {y : α → X} : Function.HasUncurry ((a : α) → Path (x a) (y a)) (α × ↑unitInterval) X

Any function φ : Π (a : α), Path (x a) (y a) can be seen as a function α × I → X.

Equations

• Path.hasUncurryPath = { uncurry := fun (φ : (a : α) → Path (x a) (y a)) (p : α × ↑unitInterval) => (φ p.1) p.2 }

@[simp]

theorem Path.refl_apply {X : Type u_1} [TopologicalSpace X] (x : X) (_t : ↑unitInterval) : (Path.refl x) _t = x

def Path.refl {X : Type u_1} [TopologicalSpace X] (x : X) : Path x x

The constant path from a point to itself

Equations

• Path.refl x = { toContinuousMap := { toFun := fun (_t : ↑unitInterval) => x, continuous_toFun := ⋯ }, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.refl_range {X : Type u_1} [TopologicalSpace X] {a : X} : Set.range ⇑(Path.refl a) = {a}

@[simp]

theorem Path.symm_apply {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : ∀ (a : ↑unitInterval), (Path.symm γ) a = (⇑γ ∘ unitInterval.symm) a

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

The reverse of a path from x to y, as a path from y to x

Equations

• Path.symm γ = { toContinuousMap := { toFun := ⇑γ ∘ unitInterval.symm, continuous_toFun := ⋯ }, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.symm_symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.symm (Path.symm γ) = γ

theorem Path.symm_bijective {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} : Function.Bijective Path.symm

@[simp]

theorem Path.refl_symm {X : Type u_1} [TopologicalSpace X] {a : X} : Path.symm (Path.refl a) = Path.refl a

@[simp]

theorem Path.symm_range {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) : Set.range ⇑(Path.symm γ) = Set.range ⇑γ

Space of paths

instance Path.topologicalSpace {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} : TopologicalSpace (Path x y)

The following instance defines the topology on the path space to be induced from the compact-open topology on the space C(I,X) of continuous maps from I to X.

Equations

• Path.topologicalSpace = TopologicalSpace.induced toContinuousMap ContinuousMap.compactOpen

theorem Path.continuous_eval {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} : Continuous fun (p : Path x y × ↑unitInterval) => p.1 p.2

theorem Continuous.path_eval {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {Y : Type u_4} [TopologicalSpace Y] {f : Y → Path x y} {g : Y → ↑unitInterval} (hf : Continuous f) (hg : Continuous g) : Continuous fun (y_1 : Y) => (f y_1) (g y_1)

theorem Path.continuous_uncurry_iff {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {Y : Type u_4} [TopologicalSpace Y] {g : Y → Path x y} : Continuous ↿g ↔ Continuous g

def Path.extend {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : ℝ → X

A continuous map extending a path to ℝ, constant before 0 and after 1.

Equations

• Path.extend γ = Set.IccExtend Path.extend.proof_1 ⇑γ

theorem Continuous.path_extend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {γ : Y → Path x y} {f : Y → ℝ} (hγ : Continuous ↿γ) (hf : Continuous f) : Continuous fun (t : Y) => Path.extend (γ t) (f t)

See Note [continuity lemma statement].

theorem Path.continuous_extend {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Continuous (Path.extend γ)

A useful special case of Continuous.path_extend.

theorem Filter.Tendsto.path_extend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {l : Y → X} {r : Y → X} {y : Y} {l₁ : Filter ℝ} {l₂ : Filter X} {γ : (y : Y) → Path (l y) (r y)} (hγ : Filter.Tendsto (↿γ) (nhds y ×ˢ Filter.map (Set.projIcc 0 1 ⋯) l₁) l₂) : Filter.Tendsto (↿fun (x : Y) => Path.extend (γ x)) (nhds y ×ˢ l₁) l₂

theorem ContinuousAt.path_extend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {g : Y → ℝ} {l : Y → X} {r : Y → X} (γ : (y : Y) → Path (l y) (r y)) {y : Y} (hγ : ContinuousAt (↿γ) (y, Set.projIcc 0 1 ⋯ (g y))) (hg : ContinuousAt g y) : ContinuousAt (fun (i : Y) => Path.extend (γ i) (g i)) y

@[simp]

theorem Path.extend_extends {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : Path.extend γ t = γ { val := t, property := ht }

theorem Path.extend_zero {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.extend γ 0 = x

theorem Path.extend_one {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.extend γ 1 = y

@[simp]

theorem Path.extend_extends' {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) (t : ↑(Set.Icc 0 1)) : Path.extend γ ↑t = γ t

@[simp]

theorem Path.extend_range {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) : Set.range (Path.extend γ) = Set.range ⇑γ

theorem Path.extend_of_le_zero {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t : ℝ} (ht : t ≤ 0) : Path.extend γ t = a

theorem Path.extend_of_one_le {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t : ℝ} (ht : 1 ≤ t) : Path.extend γ t = b

@[simp]

theorem Path.refl_extend {X : Type u_1} [TopologicalSpace X] {a : X} : Path.extend (Path.refl a) = fun (x : ℝ) => a

def Path.ofLine {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {f : ℝ → X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x) (h₁ : f 1 = y) : Path x y

The path obtained from a map defined on ℝ by restriction to the unit interval.

Equations

• Path.ofLine hf h₀ h₁ = { toContinuousMap := { toFun := f ∘ Subtype.val, continuous_toFun := ⋯ }, source' := h₀, target' := h₁ }

theorem Path.ofLine_mem {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {f : ℝ → X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x) (h₁ : f 1 = y) (t : ↑unitInterval) : (Path.ofLine hf h₀ h₁) t ∈ f '' unitInterval

def Path.trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (γ : Path x y) (γ' : Path y z) : Path x z

Concatenation of two paths from x to y and from y to z, putting the first path on [0, 1/2] and the second one on [1/2, 1].

Equations

• One or more equations did not get rendered due to their size.

theorem Path.trans_apply {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (γ : Path x y) (γ' : Path y z) (t : ↑unitInterval) : (Path.trans γ γ') t = if h : ↑t ≤ 1 / 2 then γ { val := 2 * ↑t, property := ⋯ } else γ' { val := 2 * ↑t - 1, property := ⋯ }

@[simp]

theorem Path.trans_symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (γ : Path x y) (γ' : Path y z) : Path.symm (Path.trans γ γ') = Path.trans (Path.symm γ') (Path.symm γ)

@[simp]

theorem Path.refl_trans_refl {X : Type u_1} [TopologicalSpace X] {a : X} : Path.trans (Path.refl a) (Path.refl a) = Path.refl a

theorem Path.trans_range {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} {c : X} (γ₁ : Path a b) (γ₂ : Path b c) : Set.range ⇑(Path.trans γ₁ γ₂) = Set.range ⇑γ₁ ∪ Set.range ⇑γ₂

def Path.map' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {f : X → Y} (h : ContinuousOn f (Set.range ⇑γ)) : Path (f x) (f y)

Image of a path from x to y by a map which is continuous on the path.

Equations

• Path.map' γ h = { toContinuousMap := { toFun := f ∘ ⇑γ, continuous_toFun := ⋯ }, source' := ⋯, target' := ⋯ }

def Path.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {f : X → Y} (h : Continuous f) : Path (f x) (f y)

Image of a path from x to y by a continuous map

Equations

• Path.map γ h = Path.map' γ ⋯

@[simp]

theorem Path.map_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {f : X → Y} (h : Continuous f) : ⇑(Path.map γ h) = f ∘ ⇑γ

@[simp]

theorem Path.map_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {f : X → Y} (h : Continuous f) : Path.symm (Path.map γ h) = Path.map (Path.symm γ) h

@[simp]

theorem Path.map_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {z : X} (γ : Path x y) (γ' : Path y z) {f : X → Y} (h : Continuous f) : Path.map (Path.trans γ γ') h = Path.trans (Path.map γ h) (Path.map γ' h)

@[simp]

theorem Path.map_id {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.map γ ⋯ = γ

@[simp]

theorem Path.map_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {Z : Type u_4} [TopologicalSpace Z] {f : X → Y} (hf : Continuous f) {g : Y → Z} (hg : Continuous g) : Path.map (Path.map γ hf) hg = Path.map γ ⋯

def Path.cast {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) {x' : X} {y' : X} (hx : x' = x) (hy : y' = y) : Path x' y'

Casting a path from x to y to a path from x' to y' when x' = x and y' = y

Equations

• Path.cast γ hx hy = { toContinuousMap := { toFun := ⇑γ, continuous_toFun := ⋯ }, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.symm_cast {X : Type u_1} [TopologicalSpace X] {a₁ : X} {a₂ : X} {b₁ : X} {b₂ : X} (γ : Path a₂ b₂) (ha : a₁ = a₂) (hb : b₁ = b₂) : Path.symm (Path.cast γ ha hb) = Path.cast (Path.symm γ) hb ha

@[simp]

theorem Path.trans_cast {X : Type u_1} [TopologicalSpace X] {a₁ : X} {a₂ : X} {b₁ : X} {b₂ : X} {c₁ : X} {c₂ : X} (γ : Path a₂ b₂) (γ' : Path b₂ c₂) (ha : a₁ = a₂) (hb : b₁ = b₂) (hc : c₁ = c₂) : Path.trans (Path.cast γ ha hb) (Path.cast γ' hb hc) = Path.cast (Path.trans γ γ') ha hc

@[simp]

theorem Path.cast_coe {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) {x' : X} {y' : X} (hx : x' = x) (hy : y' = y) : ⇑(Path.cast γ hx hy) = ⇑γ

theorem Path.symm_continuous_family {X : Type u_1} [TopologicalSpace X] {ι : Type u_4} [TopologicalSpace ι] {a : ι → X} {b : ι → X} (γ : (t : ι) → Path (a t) (b t)) (h : Continuous ↿γ) : Continuous ↿fun (t : ι) => Path.symm (γ t)

theorem Path.continuous_symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} : Continuous Path.symm

theorem Path.continuous_uncurry_extend_of_continuous_family {X : Type u_1} [TopologicalSpace X] {ι : Type u_4} [TopologicalSpace ι] {a : ι → X} {b : ι → X} (γ : (t : ι) → Path (a t) (b t)) (h : Continuous ↿γ) : Continuous ↿fun (t : ι) => Path.extend (γ t)

theorem Path.trans_continuous_family {X : Type u_1} [TopologicalSpace X] {ι : Type u_4} [TopologicalSpace ι] {a : ι → X} {b : ι → X} {c : ι → X} (γ₁ : (t : ι) → Path (a t) (b t)) (h₁ : Continuous ↿γ₁) (γ₂ : (t : ι) → Path (b t) (c t)) (h₂ : Continuous ↿γ₂) : Continuous ↿fun (t : ι) => Path.trans (γ₁ t) (γ₂ t)

theorem Continuous.path_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {z : X} {f : Y → Path x y} {g : Y → Path y z} : Continuous f → Continuous g → Continuous fun (t : Y) => Path.trans (f t) (g t)

theorem Path.continuous_trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} : Continuous fun (ρ : Path x y × Path y z) => Path.trans ρ.1 ρ.2

Product of paths

def Path.prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a₁ : X} {a₂ : X} {b₁ : Y} {b₂ : Y} (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : Path (a₁, b₁) (a₂, b₂)

Given a path in X and a path in Y, we can take their pointwise product to get a path in X × Y.

Equations

• Path.prod γ₁ γ₂ = { toContinuousMap := ContinuousMap.prodMk γ₁.toContinuousMap γ₂.toContinuousMap, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.prod_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a₁ : X} {a₂ : X} {b₁ : Y} {b₂ : Y} (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : ⇑(Path.prod γ₁ γ₂) = fun (t : ↑unitInterval) => (γ₁ t, γ₂ t)

theorem Path.trans_prod_eq_prod_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a₁ : X} {a₂ : X} {a₃ : X} {b₁ : Y} {b₂ : Y} {b₃ : Y} (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂) (δ₂ : Path b₂ b₃) : Path.trans (Path.prod γ₁ γ₂) (Path.prod δ₁ δ₂) = Path.prod (Path.trans γ₁ δ₁) (Path.trans γ₂ δ₂)

Path composition commutes with products

def Path.pi {ι : Type u_3} {χ : ι → Type u_4} [(i : ι) → TopologicalSpace (χ i)] {as : (i : ι) → χ i} {bs : (i : ι) → χ i} (γ : (i : ι) → Path (as i) (bs i)) : Path as bs

Given a family of paths, one in each Xᵢ, we take their pointwise product to get a path in Π i, Xᵢ.

Equations

• Path.pi γ = { toContinuousMap := ContinuousMap.pi fun (i : ι) => (γ i).toContinuousMap, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.pi_coe {ι : Type u_3} {χ : ι → Type u_4} [(i : ι) → TopologicalSpace (χ i)] {as : (i : ι) → χ i} {bs : (i : ι) → χ i} (γ : (i : ι) → Path (as i) (bs i)) : ⇑(Path.pi γ) = fun (t : ↑unitInterval) (i : ι) => (γ i) t

theorem Path.trans_pi_eq_pi_trans {ι : Type u_3} {χ : ι → Type u_4} [(i : ι) → TopologicalSpace (χ i)] {as : (i : ι) → χ i} {bs : (i : ι) → χ i} {cs : (i : ι) → χ i} (γ₀ : (i : ι) → Path (as i) (bs i)) (γ₁ : (i : ι) → Path (bs i) (cs i)) : Path.trans (Path.pi γ₀) (Path.pi γ₁) = Path.pi fun (i : ι) => Path.trans (γ₀ i) (γ₁ i)

Path composition commutes with products

Pointwise multiplication/addition of two paths in a topological (additive) group

def Path.add {X : Type u_1} [TopologicalSpace X] [Add X] [ContinuousAdd X] {a₁ : X} {b₁ : X} {a₂ : X} {b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) : Path (a₁ + a₂) (b₁ + b₂)

Pointwise addition of paths in a topological additive group.

Equations

• Path.add γ₁ γ₂ = Path.map (Path.prod γ₁ γ₂) ⋯

def Path.mul {X : Type u_1} [TopologicalSpace X] [Mul X] [ContinuousMul X] {a₁ : X} {b₁ : X} {a₂ : X} {b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) : Path (a₁ * a₂) (b₁ * b₂)

Pointwise multiplication of paths in a topological group. The additive version is probably more useful.

Equations

• Path.mul γ₁ γ₂ = Path.map (Path.prod γ₁ γ₂) ⋯

theorem Path.add_apply {X : Type u_1} [TopologicalSpace X] [Add X] [ContinuousAdd X] {a₁ : X} {b₁ : X} {a₂ : X} {b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (t : ↑unitInterval) : (Path.add γ₁ γ₂) t = γ₁ t + γ₂ t

theorem Path.mul_apply {X : Type u_1} [TopologicalSpace X] [Mul X] [ContinuousMul X] {a₁ : X} {b₁ : X} {a₂ : X} {b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (t : ↑unitInterval) : (Path.mul γ₁ γ₂) t = γ₁ t * γ₂ t

Truncating a path

def Path.truncate {X : Type u_4} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) (t₀ : ℝ) (t₁ : ℝ) : Path (Path.extend γ (min t₀ t₁)) (Path.extend γ t₁)

γ.truncate t₀ t₁ is the path which follows the path γ on the time interval [t₀, t₁] and stays still otherwise.

Equations

• Path.truncate γ t₀ t₁ = { toContinuousMap := { toFun := fun (s : ↑unitInterval) => Path.extend γ (min (max (↑s) t₀) t₁), continuous_toFun := ⋯ }, source' := ⋯, target' := ⋯ }

def Path.truncateOfLE {X : Type u_4} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t₀ : ℝ} {t₁ : ℝ} (h : t₀ ≤ t₁) : Path (Path.extend γ t₀) (Path.extend γ t₁)

γ.truncateOfLE t₀ t₁ h, where h : t₀ ≤ t₁ is γ.truncate t₀ t₁ casted as a path from γ.extend t₀ to γ.extend t₁.

Equations

• Path.truncateOfLE γ h = Path.cast (Path.truncate γ t₀ t₁) ⋯ ⋯

theorem Path.truncate_range {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t₀ : ℝ} {t₁ : ℝ} : Set.range ⇑(Path.truncate γ t₀ t₁) ⊆ Set.range ⇑γ

theorem Path.truncate_continuous_family {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) : Continuous fun (x : ℝ × ℝ × ↑unitInterval) => (Path.truncate γ x.1 x.2.1) x.2.2

For a path γ, γ.truncate gives a "continuous family of paths", by which we mean the uncurried function which maps (t₀, t₁, s) to γ.truncate t₀ t₁ s is continuous.

theorem Path.truncate_const_continuous_family {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) (t : ℝ) : Continuous ↿(Path.truncate γ t)

@[simp]

theorem Path.truncate_self {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) (t : ℝ) : Path.truncate γ t t = Path.cast (Path.refl (Path.extend γ t)) ⋯ ⋯

@[simp]

theorem Path.truncate_zero_zero {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) : Path.truncate γ 0 0 = Path.cast (Path.refl a) ⋯ ⋯

@[simp]

theorem Path.truncate_one_one {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) : Path.truncate γ 1 1 = Path.cast (Path.refl b) ⋯ ⋯

@[simp]

theorem Path.truncate_zero_one {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) : Path.truncate γ 0 1 = Path.cast γ ⋯ ⋯

Reparametrising a path

def Path.reparam {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) (f : ↑unitInterval → ↑unitInterval) (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Path x y

Given a path γ and a function f : I → I where f 0 = 0 and f 1 = 1, γ.reparam f is the path defined by γ ∘ f.

Equations

• Path.reparam γ f hfcont hf₀ hf₁ = { toContinuousMap := { toFun := ⇑γ ∘ f, continuous_toFun := ⋯ }, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.coe_reparam {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) {f : ↑unitInterval → ↑unitInterval} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : ⇑(Path.reparam γ f hfcont hf₀ hf₁) = ⇑γ ∘ f

@[simp]

theorem Path.reparam_id {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.reparam γ id ⋯ ⋯ ⋯ = γ

theorem Path.range_reparam {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) {f : ↑unitInterval → ↑unitInterval} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Set.range ⇑(Path.reparam γ f hfcont hf₀ hf₁) = Set.range ⇑γ

theorem Path.refl_reparam {X : Type u_1} [TopologicalSpace X] {x : X} {f : ↑unitInterval → ↑unitInterval} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Path.reparam (Path.refl x) f hfcont hf₀ hf₁ = Path.refl x

Being joined by a path

def Joined {X : Type u_1} [TopologicalSpace X] (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 : X} {y : X} (h : Joined x y) : Path x y

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

Equations

• Joined.somePath h = Nonempty.some h

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

theorem Joined.trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {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 : 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 : 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 : X} {y : X} {F : Set X} (h : JoinedIn F x y) : x ∈ F

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

def JoinedIn.somePath {X : Type u_1} [TopologicalSpace X] {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

• JoinedIn.somePath h = Classical.choose h

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

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

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 : 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 : 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 : X} {y : X} {F : Set X} (x_in : x ∈ F) (y_in : y ∈ F) : JoinedIn F x y ↔ Joined { val := x, property := x_in } { val := y, property := y_in }

@[simp]

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

theorem JoinedIn.mono {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {U : Set X} {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 : 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 : X} {y : X} {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 : 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 : X} {y : X} {F : Set X} (h : Inseparable x y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y

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}

@[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) : Set.Nonempty (pathComponent x)

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

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

theorem pathComponent_congr {X : Type u_1} [TopologicalSpace X] {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 : X} {y : X} {z : X} (hyz : Joined y z) (hxy : y ∈ pathComponent x) : z ∈ pathComponent x

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 ↔ Set.Nonempty F ∧ ∀ 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 Inducing.isPathConnected_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Set X} {f : X → Y} (hf : Inducing f) : IsPathConnected F ↔ IsPathConnected (f '' F)

If f : X → Y is a Inducing, 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 : 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_singleton {X : Type u_1} [TopologicalSpace X] (x : X) : IsPathConnected {x}

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

theorem IsPathConnected.preimage_coe {X : Type u_1} [TopologicalSpace X] {U : Set X} {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_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 : X) (y : X) : Path x y

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

Equations

• PathConnectedSpace.somePath x y = Nonempty.some ⋯

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

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

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 : Function.Surjective f) (hf' : Continuous f) : PathConnectedSpace Y

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

Equations

• ⋯ = ⋯

instance Real.instPathConnectedSpace : PathConnectedSpace ℝ

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

Equations

• Real.instPathConnectedSpace = ⋯

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

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

Equations

• ⋯ = ⋯

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

Locally path connected spaces

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

A topological space is locally path connected, at every point, path connected neighborhoods form a neighborhood basis.

• path_connected_basis : ∀ (x : X), Filter.HasBasis (nhds x) (fun (s : Set X) => s ∈ nhds x ∧ IsPathConnected s) id

  Each neighborhood filter has a basis of path-connected neighborhoods.

theorem locPathConnected_of_bases {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {p : ι → Prop} {s : X → ι → Set X} (h : ∀ (x : X), Filter.HasBasis (nhds x) p (s x)) (h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)) : LocPathConnectedSpace X

theorem pathConnectedSpace_iff_connectedSpace {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] : PathConnectedSpace X ↔ ConnectedSpace X

theorem pathConnected_subset_basis {X : Type u_1} [TopologicalSpace X] {x : X} [LocPathConnectedSpace X] {U : Set X} (h : IsOpen U) (hx : x ∈ U) : Filter.HasBasis (nhds x) (fun (s : Set X) => s ∈ nhds x ∧ IsPathConnected s ∧ s ⊆ U) id

theorem locPathConnected_of_isOpen {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {U : Set X} (h : IsOpen U) : LocPathConnectedSpace ↑U

theorem IsOpen.isConnected_iff_isPathConnected {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {U : Set X} (U_op : IsOpen U) : IsPathConnected U ↔ IsConnected U