mathlib documentation

topology.path_connected

Path connectedness

Main definitions

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

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

 Main theorems

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

For locally path connected spaces, we have

Implementation notes

By default, all paths have I as their source and X as their target, but there is an operation I_extend that will extend any continuous map γ : I → X into a continuous map I_extend γ : ℝ → 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, +∞).

The unit interval

theorem Icc_zero_one_symm {t : } :
t set.Icc 0 1 1 - t set.Icc 0 1

@[instance]

Equations
@[simp]
theorem coe_I_zero  :
0 = 0

@[instance]
def I_has_one  :

Equations
@[simp]
theorem coe_I_one  :
1 = 1

def I_symm  :
(set.Icc 0 1)(set.Icc 0 1)

Unit interval central symmetry.

Equations
@[simp]
theorem I_symm_zero  :
I_symm 0 = 1

@[simp]
theorem I_symm_one  :
I_symm 1 = 0

def proj_I  :
(set.Icc 0 1)

Projection of onto its unit interval.

Equations
theorem proj_I_I {t : } (h : t set.Icc 0 1) :
proj_I t = t, h⟩

theorem proj_I_zero  :
proj_I 0 = 0

theorem proj_I_one  :
proj_I 1 = 1

def I_extend {β : Type u_1} :
((set.Icc 0 1) → β) → β

Extension of a function defined on the unit interval to , by precomposing with the projection.

Equations
theorem continuous.I_extend {X : Type u_1} [topological_space X] {f : (set.Icc 0 1) → X} :

theorem I_extend_extends {β : Type u_3} (f : (set.Icc 0 1) → β) {t : } (ht : t set.Icc 0 1) :
I_extend f t = f t, ht⟩

@[simp]
theorem I_extend_zero {β : Type u_3} (f : (set.Icc 0 1) → β) :
I_extend f 0 = f 0

@[simp]
theorem I_extend_one {β : Type u_3} (f : (set.Icc 0 1) → β) :
I_extend f 1 = f 1

@[simp]
theorem I_extend_range {β : Type u_3} (f : (set.Icc 0 1) → β) :

Paths

@[nolint]
structure path {X : Type u_1} [topological_space X] :
X → X → Type u_1

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

@[instance]
def path.has_coe_to_fun {X : Type u_1} [topological_space X] {x y : X} :

Equations
@[ext]
theorem path.ext {X : Type u_1} [topological_space X] {x y : X} {γ₁ γ₂ : path x y} :
γ₁ = γ₂γ₁ = γ₂

theorem path.continuous {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) :

@[simp]
theorem path.source {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) :
γ 0 = x

@[simp]
theorem path.target {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) :
γ 1 = y

@[instance]
def path.has_uncurry_path {X : Type u_1} {α : Type u_2} [topological_space X] {x y : α → X} :
function.has_uncurry (Π (a : α), path (x a) (y a)) × (set.Icc 0 1)) X

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

Equations
def path.refl {X : Type u_1} [topological_space X] (x : X) :
path x x

The constant path from a point to itself

Equations
@[simp]
theorem path.refl_range {X : Type u_1} [topological_space X] {a : X} :

def path.symm {X : Type u_1} [topological_space X] {x y : X} :
path x ypath y x

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

Equations
@[simp]
theorem path.refl_symm {X : Type u_1} [topological_space X] {a : X} :

@[simp]
theorem path.symm_range {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) :

def path.extend {X : Type u_1} [topological_space X] {x y : X} :
path x y → X

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

Equations
theorem path.continuous_extend {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) :

@[simp]
theorem path.extend_zero {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) :
γ.extend 0 = x

@[simp]
theorem path.extend_one {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) :
γ.extend 1 = y

@[simp]
theorem path.extend_extends {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) {t : } (ht : t set.Icc 0 1) :
γ.extend t = γ t, ht⟩

@[simp]
theorem path.extend_extends' {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) (t : (set.Icc 0 1)) :
γ.extend t = γ t

@[simp]
theorem path.extend_range {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) :

theorem path.extend_le_zero {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) {t : } :
t 0γ.extend t = a

theorem path.extend_one_le {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) {t : } :
1 tγ.extend t = b

@[simp]
theorem path.refl_extend {X : Type u_1} [topological_space X] {a : X} :
(path.refl a).extend = λ (_x : ), a

def path.of_line {X : Type u_1} [topological_space X] {x y : X} {f : → X} :
continuous_on f (set.Icc 0 1)f 0 = xf 1 = ypath x y

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

Equations
theorem path.of_line_mem {X : Type u_1} [topological_space X] {x y : X} {f : → X} (hf : continuous_on f (set.Icc 0 1)) (h₀ : f 0 = x) (h₁ : f 1 = y) (t : (set.Icc 0 1)) :
(path.of_line hf h₀ h₁) t f '' set.Icc 0 1

def path.trans {X : Type u_1} [topological_space X] {x y z : X} :
path x ypath y zpath 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
@[simp]
theorem path.refl_trans_refl {X : Type u_1} [topological_space X] {a : X} :

theorem path.trans_range {X : Type u_1} [topological_space X] {a b c : X} (γ₁ : path a b) (γ₂ : path b c) :
set.range (γ₁.trans γ₂) = set.range γ₁ set.range γ₂

def path.map {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) {Y : Type u_2} [topological_space Y] {f : X → Y} :
continuous fpath (f x) (f y)

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

Equations
@[simp]
theorem path.map_coe {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) {Y : Type u_2} [topological_space Y] {f : X → Y} (h : continuous f) :
(γ.map h) = f γ

def path.cast {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) {x' y' : X} :
x' = xy' = ypath x' y'

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

Equations
@[simp]
theorem path.symm_cast {X : Type u_1} [topological_space X] {a₁ a₂ b₁ b₂ : X} (γ : path a₂ b₂) (ha : a₁ = a₂) (hb : b₁ = b₂) :
(γ.cast ha hb).symm = γ.symm.cast hb ha

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

@[simp]
theorem path.cast_coe {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) {x' y' : X} (hx : x' = x) (hy : y' = y) :
(γ.cast hx hy) = γ

theorem path.symm_continuous_family {X : Type u_1} {ι : Type u_2} [topological_space X] [topological_space ι] {a b : ι → X} (γ : Π (t : ι), path (a t) (b t)) :
continuous γcontinuous (λ (t : ι), (γ t).symm)

theorem path.continuous_uncurry_extend_of_continuous_family {X : Type u_1} {ι : Type u_2} [topological_space X] [topological_space ι] {a b : ι → X} (γ : Π (t : ι), path (a t) (b t)) :
continuous γcontinuous (λ (t : ι), (γ t).extend)

theorem path.trans_continuous_family {X : Type u_1} {ι : Type u_2} [topological_space X] [topological_space ι] {a b c : ι → X} (γ₁ : Π (t : ι), path (a t) (b t)) (h₁ : continuous γ₁) (γ₂ : Π (t : ι), path (b t) (c t)) :
continuous γ₂continuous (λ (t : ι), (γ₁ t).trans (γ₂ t))

Truncating a path

def path.truncate {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) (t₀ t₁ : ) :
path (γ.extend (min t₀ t₁)) (γ.extend t₁)

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

Equations
def path.truncate_of_le {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) {t₀ t₁ : } :
t₀ t₁path (γ.extend t₀) (γ.extend t₁)

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

Equations
theorem path.truncate_range {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) {t₀ t₁ : } :

theorem path.truncate_continuous_family {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) :
continuous (λ (x : × × (set.Icc 0 1)), (γ.truncate x.fst x.snd.fst) x.snd.snd)

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} [topological_space X] {a b : X} (γ : path a b) (t : ) :

@[simp]
theorem path.truncate_self {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) (t : ) :
γ.truncate t t = (path.refl (γ.extend t)).cast _ rfl

@[simp]
theorem path.truncate_zero_zero {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) :
γ.truncate 0 0 = (path.refl a).cast _ _

@[simp]
theorem path.truncate_one_one {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) :
γ.truncate 1 1 = (path.refl b).cast _ _

@[simp]
theorem path.truncate_zero_one {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) :
γ.truncate 0 1 = γ.cast _ _

Being joined by a path

def joined {X : Type u_1} [topological_space X] :
X → X → Prop

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

Equations
theorem joined.refl {X : Type u_1} [topological_space X] (x : X) :
joined x x

def joined.some_path {X : Type u_1} [topological_space X] {x y : X} :
joined x ypath x y

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

Equations
theorem joined.symm {X : Type u_1} [topological_space X] {x y : X} :
joined x yjoined y x

theorem joined.trans {X : Type u_1} [topological_space X] {x y z : X} :
joined x yjoined y zjoined x z

def path_setoid (X : Type u_1) [topological_space X] :

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

Equations
def zeroth_homotopy (X : Type u_1) [topological_space X] :
Type u_1

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

Equations

Being joined by a path inside a set

def joined_in {X : Type u_1} [topological_space X] :
set XX → 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
theorem joined_in.mem {X : Type u_1} [topological_space X] {x y : X} {F : set X} :
joined_in F x yx F y F

theorem joined_in.source_mem {X : Type u_1} [topological_space X] {x y : X} {F : set X} :
joined_in F x yx F

theorem joined_in.target_mem {X : Type u_1} [topological_space X] {x y : X} {F : set X} :
joined_in F x yy F

def joined_in.some_path {X : Type u_1} [topological_space X] {x y : X} {F : set X} :
joined_in F x ypath x y

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

Equations
theorem joined_in.some_path_mem {X : Type u_1} [topological_space X] {x y : X} {F : set X} (h : joined_in F x y) (t : (set.Icc 0 1)) :

theorem joined_in.joined_subtype {X : Type u_1} [topological_space X] {x y : X} {F : set X} (h : joined_in 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 joined_in.of_line {X : Type u_1} [topological_space X] {x y : X} {F : set X} {f : → X} :
continuous_on f (set.Icc 0 1)f 0 = xf 1 = yf '' set.Icc 0 1 Fjoined_in F x y

theorem joined_in.joined {X : Type u_1} [topological_space X] {x y : X} {F : set X} :
joined_in F x yjoined x y

theorem joined_in_iff_joined {X : Type u_1} [topological_space X] {x y : X} {F : set X} (x_in : x F) (y_in : y F) :
joined_in F x y joined x, x_in⟩ y, y_in⟩

@[simp]
theorem joined_in_univ {X : Type u_1} [topological_space X] {x y : X} :

theorem joined_in.mono {X : Type u_1} [topological_space X] {x y : X} {U V : set X} :
joined_in U x yU Vjoined_in V x y

theorem joined_in.refl {X : Type u_1} [topological_space X] {x : X} {F : set X} :
x Fjoined_in F x x

theorem joined_in.symm {X : Type u_1} [topological_space X] {x y : X} {F : set X} :
joined_in F x yjoined_in F y x

theorem joined_in.trans {X : Type u_1} [topological_space X] {x y z : X} {F : set X} :
joined_in F x yjoined_in F y zjoined_in F x z

Path component

def path_component {X : Type u_1} [topological_space X] :
X → set X

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

Equations
@[simp]
theorem mem_path_component_self {X : Type u_1} [topological_space X] (x : X) :

@[simp]
theorem path_component.nonempty {X : Type u_1} [topological_space X] (x : X) :

theorem mem_path_component_of_mem {X : Type u_1} [topological_space X] {x y : X} :

theorem path_component_symm {X : Type u_1} [topological_space X] {x y : X} :

theorem path_component_congr {X : Type u_1} [topological_space X] {x y : X} :

def path_component_in {X : Type u_1} [topological_space X] :
X → set Xset X

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

Equations
@[simp]

theorem joined.mem_path_component {X : Type u_1} [topological_space X] {x y z : X} :

Path connected sets

def is_path_connected {X : Type u_1} [topological_space X] :
set X → Prop

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

Equations
theorem is_path_connected_iff_eq {X : Type u_1} [topological_space X] {F : set X} :
is_path_connected F ∃ (x : X) (H : x F), path_component_in x F = F

theorem is_path_connected.joined_in {X : Type u_1} [topological_space X] {F : set X} (h : is_path_connected F) (x y : X) :
x Fy Fjoined_in F x y

theorem is_path_connected_iff {X : Type u_1} [topological_space X] {F : set X} :
is_path_connected F F.nonempty ∀ (x y : X), x Fy Fjoined_in F x y

theorem is_path_connected.image {X : Type u_1} [topological_space X] {F : set X} {Y : Type u_2} [topological_space Y] (hF : is_path_connected F) {f : X → Y} :

theorem is_path_connected.mem_path_component {X : Type u_1} [topological_space X] {x y : X} {F : set X} :
is_path_connected Fx Fy Fy path_component x

theorem is_path_connected.subset_path_component {X : Type u_1} [topological_space X] {x : X} {F : set X} :

theorem is_path_connected.union {X : Type u_1} [topological_space X] {U V : set X} :

theorem is_path_connected.preimage_coe {X : Type u_1} [topological_space X] {U W : set X} :

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 is_path_connected.exists_path_through_family {X : Type u_1} [topological_space X] {n : } {s : set X} (h : is_path_connected s) (p : fin (n + 1) → X) :
(∀ (i : fin (n + 1)), p i s)(∃ (γ : path (p 0) (p n)), set.range γ s ∀ (i : fin (n + 1)), p i set.range γ)

theorem is_path_connected.exists_path_through_family' {X : Type u_1} [topological_space X] {n : } {s : set X} (h : is_path_connected s) (p : fin (n + 1) → X) :
(∀ (i : fin (n + 1)), p i s)(∃ (γ : path (p 0) (p n)) (t : fin (n + 1)(set.Icc 0 1)), (∀ (t : (set.Icc 0 1)), γ t s) ∀ (i : fin (n + 1)), γ (t i) = p i)

Path connected spaces

@[class]
structure path_connected_space (X : Type u_4) [topological_space X] :
Prop

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

Instances
def path_connected_space.some_path {X : Type u_1} [topological_space X] [path_connected_space X] (x y : X) :
path x y

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

Equations
theorem path_connected_space.exists_path_through_family {X : Type u_1} [topological_space X] [path_connected_space X] {n : } (p : fin (n + 1) → X) :
∃ (γ : path (p 0) (p n)), ∀ (i : fin (n + 1)), p i set.range γ

theorem path_connected_space.exists_path_through_family' {X : Type u_1} [topological_space X] [path_connected_space X] {n : } (p : fin (n + 1) → X) :
∃ (γ : path (p 0) (p n)) (t : fin (n + 1)(set.Icc 0 1)), ∀ (i : fin (n + 1)), γ (t i) = p i

Locally path connected spaces

@[class]
structure loc_path_connected_space (X : Type u_4) [topological_space X] :
Prop

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

Instances
theorem loc_path_connected_of_bases {X : Type u_1} [topological_space X] {ι : Type u_2} {p : ι → Prop} {s : X → ι → set X} :
(∀ (x : X), (𝓝 x).has_basis p (s x))(∀ (x : X) (i : ι), p iis_path_connected (s x i))loc_path_connected_space X

theorem path_connected_subset_basis {X : Type u_1} [topological_space X] {x : X} [loc_path_connected_space X] {U : set X} :
is_open Ux U(𝓝 x).has_basis (λ (s : set X), s 𝓝 x is_path_connected s s U) id