mathlib3 documentation

topology.path_connected

Path connectedness #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.some_path (h : joined x y) selects some path between two points x and y.
path_component (x : X) is the set of points joined to x.
path_connected_space 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.

joined_in F (x y : X) means there is a path γ joining x to y with values in F.
joined_in.some_path (h : joined_in F x y) selects a path from x to y inside F.
path_component_in F (x : X) is the set of points joined to x in F.
is_path_connected F asserts that F is non-empty and every two points of F are joined in F.
loc_path_connected_space 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 joined_in F are transitive relations.

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

path_connected_space_iff_univ : path_connected_space X ↔ is_path_connected (univ : set X)
is_path_connected_iff_path_connected_space : is_path_connected F ↔ path_connected_space ↥F

For locally path connected spaces, we have

path_connected_space_iff_connected_space : path_connected_space X ↔ connected_space X
is_connected_iff_is_path_connected (U_op : is_open U) : is_path_connected U ↔ is_connected U

Implementation notes #

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

@[nolint]

structure path {X : Type u_1} [topological_space X] (x y : X) :

Type u_1

to_continuous_map : C(↥unit_interval , X)
source' : self.to_continuous_map.to_fun 0 = x
target' : self.to_continuous_map.to_fun 1 = y

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

Instances for path

@[protected, instance]

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

has_coe_to_fun (path x y) (λ (_x : path x y), ↥unit_interval → X)

Equations

path.has_coe_to_fun = {coe := λ (p : path x y), p.to_continuous_map.to_fun}

@[protected, ext]

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

⇑γ₁ = ⇑γ₂ → γ₁ = γ₂

@[simp]

theorem path.coe_mk {X : Type u_1} [topological_space X] {x y : X} (f : ↥unit_interval → X) (h₁ : continuous f . "continuity'") (h₂ : {to_fun := f, continuous_to_fun := h₁}.to_fun 0 = x) (h₃ : {to_fun := f, continuous_to_fun := h₁}.to_fun 1 = y) :

⇑{to_continuous_map := {to_fun := f, continuous_to_fun := h₁}, source' := h₂, target' := h₃} = f

@[protected, continuity]

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

continuous ⇑γ

@[protected, simp]

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

⇑γ 0 = x

@[protected, simp]

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

⇑γ 1 = y

def path.simps.apply {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) :

↥unit_interval → 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_to_continuous_map {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) :

⇑(γ.to_continuous_map) = ⇑γ

@[protected, 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)) (α × ↥unit_interval) X

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

Equations

path.has_uncurry_path = {uncurry := λ (φ : Π (a : α), path (x a) (y a)) (p : α × ↥unit_interval), ⇑(φ p.fst) p.snd}

@[refl]

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

path x x

The constant path from a point to itself

Equations

path.refl x = {to_continuous_map := {to_fun := λ (t : ↥unit_interval), x, continuous_to_fun := _}, source' := _, target' := _}

@[simp]

theorem path.refl_apply {X : Type u_1} [topological_space X] (x : X) (t : ↥unit_interval) :

⇑(path.refl x) t = x

@[simp]

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

set.range ⇑(path.refl a) = {a}

@[symm]

def path.symm {X : Type u_1} [topological_space 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

γ.symm = {to_continuous_map := {to_fun := ⇑γ ∘ unit_interval.symm, continuous_to_fun := _}, source' := _, target' := _}

@[simp]

theorem path.symm_apply {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) (ᾰ : ↥unit_interval) :

⇑(γ.symm) ᾰ = (⇑γ ∘ unit_interval.symm) ᾰ

@[simp]

theorem path.symm_symm {X : Type u_1} [topological_space X] {x y : X} {γ : path x y} :

γ.symm.symm = γ

@[simp]

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

(path.refl a).symm = path.refl a

@[simp]

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

set.range ⇑(γ.symm) = set.range ⇑γ

Space of paths #

@[protected, instance]

def path.continuous_map.has_coe {X : Type u_1} [topological_space X] {x y : X} :

has_coe (path x y) C(↥unit_interval , X)

Equations

path.continuous_map.has_coe = {coe := λ (γ : path x y), γ.to_continuous_map}

@[protected, instance]

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

topological_space (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.topological_space = topological_space.induced coe continuous_map.compact_open

theorem path.continuous_eval {X : Type u_1} [topological_space X] {x y : X} :

continuous (λ (p : path x y × ↥unit_interval), ⇑(p.fst) p.snd)

@[continuity]

theorem continuous.path_eval {X : Type u_1} [topological_space X] {x y : X} {Y : Type u_2} [topological_space Y] {f : Y → path x y} {g : Y → ↥unit_interval} (hf : continuous f) (hg : continuous g) :

continuous (λ (y_1 : Y), ⇑(f y_1) (g y_1))

theorem path.continuous_uncurry_iff {X : Type u_1} [topological_space X] {x y : X} {Y : Type u_2} [topological_space Y] {g : Y → path x y} :

continuous ↿g ↔ continuous g

noncomputable def path.extend {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) :

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

Equations

γ.extend = set.Icc_extend path.extend._proof_1 ⇑γ

theorem continuous.path_extend {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {γ : Y → path x y} {f : Y → ℝ} (hγ : continuous ↿γ) (hf : continuous f) :

continuous (λ (t : Y), (γ t).extend (f t))

See Note [continuity lemma statement].

@[continuity]

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

continuous γ.extend

A useful special case of continuous.path_extend.

theorem filter.tendsto.path_extend {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {l r : Y → X} {y : Y} {l₁ : filter ℝ} {l₂ : filter X} {γ : Π (y : Y), path (l y) (r y)} (hγ : filter.tendsto ↿γ ((nhds y).prod (filter.map (set.proj_Icc 0 1 zero_le_one) l₁)) l₂) :

filter.tendsto ↿(λ (x : Y), (γ x).extend) ((nhds y).prod l₁) l₂

theorem continuous_at.path_extend {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {g : Y → ℝ} {l r : Y → X} (γ : Π (y : Y), path (l y) (r y)) {y : Y} (hγ : continuous_at ↿γ (y, set.proj_Icc 0 1 zero_le_one (g y))) (hg : continuous_at g y) :

continuous_at (λ (i : Y), (γ i).extend (g i)) 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⟩

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

γ.extend 0 = x

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 : ↥(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) :

set.range γ.extend = set.range ⇑γ

theorem path.extend_of_le_zero {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) {t : ℝ} (ht : t ≤ 0) :

γ.extend t = a

theorem path.extend_of_one_le {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) {t : ℝ} (ht : 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} (hf : continuous_on f unit_interval) (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.of_line hf h₀ h₁ = {to_continuous_map := {to_fun := f ∘ coe, continuous_to_fun := _}, source' := h₀, target' := h₁}

theorem path.of_line_mem {X : Type u_1} [topological_space X] {x y : X} {f : ℝ → X} (hf : continuous_on f unit_interval) (h₀ : f 0 = x) (h₁ : f 1 = y) (t : ↥unit_interval) :

⇑(path.of_line hf h₀ h₁) t ∈ f '' unit_interval

@[trans]

noncomputable def path.trans {X : Type u_1} [topological_space X] {x y 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

γ.trans γ' = {to_continuous_map := {to_fun := (λ (t : ℝ), ite (t ≤ 1 / 2) (γ.extend (2 * t)) (γ'.extend (2 * t - 1))) ∘ coe, continuous_to_fun := _}, source' := _, target' := _}

theorem path.trans_apply {X : Type u_1} [topological_space X] {x y z : X} (γ : path x y) (γ' : path y z) (t : ↥unit_interval) :

⇑(γ.trans γ') t = dite (↑t ≤ 1 / 2) (λ (h : ↑t ≤ 1 / 2), ⇑γ ⟨2 * ↑t, _⟩) (λ (h : ¬↑t ≤ 1 / 2), ⇑γ' ⟨2 * ↑t - 1, _⟩)

@[simp]

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

(γ.trans γ').symm = γ'.symm.trans γ.symm

@[simp]

theorem path.refl_trans_refl {X : Type u_1} [topological_space X] {a : X} :

(path.refl a).trans (path.refl a) = path.refl a

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} (h : continuous f) :

path (f x) (f y)

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

Equations

γ.map h = {to_continuous_map := {to_fun := f ∘ ⇑γ, continuous_to_fun := _}, source' := _, target' := _}

@[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 ∘ ⇑γ

@[simp]

theorem path.map_symm {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).symm = γ.symm.map h

@[simp]

theorem path.map_trans {X : Type u_1} [topological_space X] {x y z : X} (γ : path x y) (γ' : path y z) {Y : Type u_2} [topological_space Y] {f : X → Y} (h : continuous f) :

(γ.trans γ').map h = (γ.map h).trans (γ'.map h)

@[simp]

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

γ.map continuous_id = γ

@[simp]

theorem path.map_map {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) {Y : Type u_2} [topological_space Y] {Z : Type u_3} [topological_space Z] {f : X → Y} (hf : continuous f) {g : Y → Z} (hg : continuous g) :

(γ.map hf).map hg = γ.map _

def path.cast {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) {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

γ.cast hx hy = {to_continuous_map := {to_fun := ⇑γ, continuous_to_fun := _}, source' := _, target' := _}

@[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) = ⇑γ

@[continuity]

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)) (h : continuous ↿γ) :

continuous ↿(λ (t : ι), (γ t).symm)

@[continuity]

theorem path.continuous_symm {X : Type u_1} [topological_space X] {x y : X} :

continuous path.symm

@[continuity]

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)) (h : continuous ↿γ) :

continuous ↿(λ (t : ι), (γ t).extend)

@[continuity]

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)) (h₂ : continuous ↿γ₂) :

continuous ↿(λ (t : ι), (γ₁ t).trans (γ₂ t))

@[continuity]

theorem continuous.path_trans {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y z : X} {f : Y → path x y} {g : Y → path y z} :

continuous f → continuous g → continuous (λ (t : Y), (f t).trans (g t))

@[continuity]

theorem path.continuous_trans {X : Type u_1} [topological_space X] {x y z : X} :

continuous (λ (ρ : path x y × path y z), ρ.fst.trans ρ.snd)

Product of paths #

@[protected]

def path.prod {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {a₁ a₂ : X} {b₁ 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

γ₁.prod γ₂ = {to_continuous_map := γ₁.to_continuous_map.prod_mk γ₂.to_continuous_map, source' := _, target' := _}

@[simp]

theorem path.prod_coe_fn {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {a₁ a₂ : X} {b₁ b₂ : Y} (γ₁ : path a₁ a₂) (γ₂ : path b₁ b₂) :

⇑(γ₁.prod γ₂) = λ (t : ↥unit_interval), (⇑γ₁ t, ⇑γ₂ t)

theorem path.trans_prod_eq_prod_trans {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {a₁ a₂ a₃ : X} {b₁ b₂ b₃ : Y} (γ₁ : path a₁ a₂) (δ₁ : path a₂ a₃) (γ₂ : path b₁ b₂) (δ₂ : path b₂ b₃) :

(γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)

Path composition commutes with products

@[protected]

def path.pi {ι : Type u_3} {χ : ι → Type u_4} [Π (i : ι), topological_space (χ i)] {as 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 γ = {to_continuous_map := continuous_map.pi (λ (i : ι), (γ i).to_continuous_map), source' := _, target' := _}

@[simp]

theorem path.pi_coe_fn {ι : Type u_3} {χ : ι → Type u_4} [Π (i : ι), topological_space (χ i)] {as bs : Π (i : ι), χ i} (γ : Π (i : ι), path (as i) (bs i)) :

⇑(path.pi γ) = λ (t : ↥unit_interval) (i : ι), ⇑(γ i) t

theorem path.trans_pi_eq_pi_trans {ι : Type u_3} {χ : ι → Type u_4} [Π (i : ι), topological_space (χ i)] {as bs cs : Π (i : ι), χ i} (γ₀ : Π (i : ι), path (as i) (bs i)) (γ₁ : Π (i : ι), path (bs i) (cs i)) :

(path.pi γ₀).trans (path.pi γ₁) = path.pi (λ (i : ι), (γ₀ i).trans (γ₁ i))

Path composition commutes with products

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

@[protected]

def path.add {X : Type u_1} [topological_space X] [has_add X] [has_continuous_add X] {a₁ b₁ a₂ b₂ : X} (γ₁ : path a₁ b₁) (γ₂ : path a₂ b₂) :

path (a₁ + a₂) (b₁ + b₂)

Pointwise addition of paths in a topological additive group.

Equations

γ₁.add γ₂ = (γ₁.prod γ₂).map continuous_add

@[protected]

def path.mul {X : Type u_1} [topological_space X] [has_mul X] [has_continuous_mul X] {a₁ b₁ a₂ 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

γ₁.mul γ₂ = (γ₁.prod γ₂).map continuous_mul

@[protected]

theorem path.mul_apply {X : Type u_1} [topological_space X] [has_mul X] [has_continuous_mul X] {a₁ b₁ a₂ b₂ : X} (γ₁ : path a₁ b₁) (γ₂ : path a₂ b₂) (t : ↥unit_interval) :

⇑(γ₁.mul γ₂) t = ⇑γ₁ t * ⇑γ₂ t

@[protected]

theorem path.add_apply {X : Type u_1} [topological_space X] [has_add X] [has_continuous_add X] {a₁ b₁ a₂ b₂ : X} (γ₁ : path a₁ b₁) (γ₂ : path a₂ b₂) (t : ↥unit_interval) :

⇑(γ₁.add γ₂) t = ⇑γ₁ t + ⇑γ₂ t

Truncating a path #

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

path (γ.extend (linear_order.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

γ.truncate t₀ t₁ = {to_continuous_map := {to_fun := λ (s : ↥unit_interval), γ.extend (linear_order.min (linear_order.max ↑s t₀) t₁), continuous_to_fun := _}, source' := _, target' := _}

noncomputable def path.truncate_of_le {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) {t₀ t₁ : ℝ} (h : 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

γ.truncate_of_le h = (γ.truncate t₀ t₁).cast _ _

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

set.range ⇑(γ.truncate t₀ t₁) ⊆ set.range ⇑γ

@[continuity]

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

continuous (λ (x : ℝ × ℝ × ↥unit_interval), ⇑(γ.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.

@[continuity]

theorem path.truncate_const_continuous_family {X : Type u_1} [topological_space X] {a b : X} (γ : path a b) (t : ℝ) :

continuous ↿(γ.truncate 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 _ _

Reparametrising a path #

def path.reparam {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) (f : ↥unit_interval → ↥unit_interval) (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

γ.reparam f hfcont hf₀ hf₁ = {to_continuous_map := {to_fun := ⇑γ ∘ f, continuous_to_fun := _}, source' := _, target' := _}

@[simp]

theorem path.coe_to_fun {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) {f : ↥unit_interval → ↥unit_interval} (hfcont : continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :

⇑(γ.reparam f hfcont hf₀ hf₁) = ⇑γ ∘ f

@[simp]

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

γ.reparam id continuous_id rfl rfl = γ

theorem path.range_reparam {X : Type u_1} [topological_space X] {x y : X} (γ : path x y) {f : ↥unit_interval → ↥unit_interval} (hfcont : continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :

set.range ⇑(γ.reparam f hfcont hf₀ hf₁) = set.range ⇑γ

theorem path.refl_reparam {X : Type u_1} [topological_space X] {x : X} {f : ↥unit_interval → ↥unit_interval} (hfcont : continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :

(path.refl x).reparam f hfcont hf₀ hf₁ = path.refl x

Being joined by a path #

def joined {X : Type u_1} [topological_space 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)

@[refl]

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

noncomputable def joined.some_path {X : Type u_1} [topological_space X] {x y : X} (h : joined x y) :

path x y

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

Equations

h.some_path = nonempty.some h

@[symm]

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

@[trans]

theorem joined.trans {X : Type u_1} [topological_space X] {x y z : X} (hxy : joined x y) (hyz : joined y 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

path_setoid X = {r := joined _inst_1, iseqv := _}

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

zeroth_homotopy X = quotient (path_setoid X)

Instances for zeroth_homotopy

zeroth_homotopy.inhabited

@[protected, instance]

def zeroth_homotopy.inhabited :

inhabited (zeroth_homotopy ℝ)

Equations

zeroth_homotopy.inhabited = {default := ⟦0⟧}

Being joined by a path inside a set #

def joined_in {X : Type u_1} [topological_space X] (F : set X) (x y : X) :

Prop

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

Equations

joined_in F x y = ∃ (γ : path x y), ∀ (t : ↥unit_interval), ⇑γ t ∈ F

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

x ∈ F ∧ y ∈ F

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

x ∈ F

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

y ∈ F

noncomputable def joined_in.some_path {X : Type u_1} [topological_space X] {x y : X} {F : set X} (h : joined_in F x y) :

path x y

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

Equations

h.some_path = classical.some h

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 : ↥unit_interval) :

⇑(h.some_path) t ∈ F

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} (hf : continuous_on f unit_interval) (h₀ : f 0 = x) (h₁ : f 1 = y) (hF : f '' unit_interval ⊆ F) :

joined_in F x y

theorem joined_in.joined {X : Type u_1} [topological_space X] {x y : X} {F : set X} (h : joined_in F 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} :

joined_in set.univ x y ↔ joined x y

theorem joined_in.mono {X : Type u_1} [topological_space X] {x y : X} {U V : set X} (h : joined_in U x y) (hUV : U ⊆ V) :

joined_in V x y

theorem joined_in.refl {X : Type u_1} [topological_space X] {x : X} {F : set X} (h : x ∈ F) :

joined_in F x x

@[symm]

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

joined_in F y x

theorem joined_in.trans {X : Type u_1} [topological_space X] {x y z : X} {F : set X} (hxy : joined_in F x y) (hyz : joined_in F y z) :

joined_in F x z

Path component #

def path_component {X : Type u_1} [topological_space X] (x : X) :

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

Equations

path_component x = {y : X | joined x y}

@[simp]

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

x ∈ path_component x

@[simp]

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

(path_component x).nonempty

theorem mem_path_component_of_mem {X : Type u_1} [topological_space X] {x y : X} (h : x ∈ path_component y) :

y ∈ path_component x

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

x ∈ path_component y ↔ y ∈ path_component x

theorem path_component_congr {X : Type u_1} [topological_space X] {x y : X} (h : x ∈ path_component y) :

path_component x = path_component y

theorem path_component_subset_component {X : Type u_1} [topological_space X] (x : X) :

path_component x ⊆ connected_component x

def path_component_in {X : Type u_1} [topological_space X] (x : X) (F : set X) :

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

Equations

path_component_in x F = {y : X | joined_in F x y}

@[simp]

theorem path_component_in_univ {X : Type u_1} [topological_space X] (x : X) :

path_component_in x set.univ = path_component x

theorem joined.mem_path_component {X : Type u_1} [topological_space X] {x y z : X} (hyz : joined y z) (hxy : y ∈ path_component x) :

z ∈ path_component x

Path connected sets #

def is_path_connected {X : Type u_1} [topological_space 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

is_path_connected F = ∃ (x : X) (H : x ∈ F), ∀ {y : X}, y ∈ F → joined_in F x y

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 : X) (H : x ∈ F) (y : X) (H_1 : y ∈ F) :

joined_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 : X), x ∈ F → ∀ (y : X), y ∈ F → joined_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} (hf : continuous f) :

is_path_connected (f '' F)

theorem is_path_connected.mem_path_component {X : Type u_1} [topological_space X] {x y : X} {F : set X} (h : is_path_connected F) (x_in : x ∈ F) (y_in : y ∈ F) :

y ∈ path_component x

theorem is_path_connected.subset_path_component {X : Type u_1} [topological_space X] {x : X} {F : set X} (h : is_path_connected F) (x_in : x ∈ F) :

F ⊆ path_component x

theorem is_path_connected.union {X : Type u_1} [topological_space X] {U V : set X} (hU : is_path_connected U) (hV : is_path_connected V) (hUV : (U ∩ V).nonempty) :

is_path_connected (U ∪ V)

theorem is_path_connected.preimage_coe {X : Type u_1} [topological_space X] {U W : set X} (hW : is_path_connected W) (hWU : W ⊆ U) :

is_path_connected (coe ⁻¹' 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 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) (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 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) (hp : ∀ (i : fin (n + 1)), p i ∈ s) :

∃ (γ : path (p 0) (p ↑n)) (t : fin (n + 1) → ↥unit_interval), (∀ (t : ↥unit_interval), ⇑γ 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

nonempty : nonempty X
joined : ∀ (x y : X), joined x y

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

Instances of this typeclass

theorem path_connected_space_iff_zeroth_homotopy {X : Type u_1} [topological_space X] :

path_connected_space X ↔ nonempty (zeroth_homotopy X) ∧ subsingleton (zeroth_homotopy X)

noncomputable 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

path_connected_space.some_path x y = nonempty.some _

theorem is_path_connected_iff_path_connected_space {X : Type u_1} [topological_space X] {F : set X} :

is_path_connected F ↔ path_connected_space ↥F

theorem path_connected_space_iff_univ {X : Type u_1} [topological_space X] :

path_connected_space X ↔ is_path_connected set.univ

theorem path_connected_space_iff_eq {X : Type u_1} [topological_space X] :

path_connected_space X ↔ ∃ (x : X), path_component x = set.univ

@[protected, instance]

def path_connected_space.connected_space {X : Type u_1} [topological_space X] [path_connected_space X] :

connected_space X

theorem is_path_connected.is_connected {X : Type u_1} [topological_space X] {F : set X} (hF : is_path_connected F) :

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) → ↥unit_interval), ∀ (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

path_connected_basis : ∀ (x : X), (nhds x).has_basis (λ (s : set X), s ∈ nhds x ∧ is_path_connected s) id

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

Instances of this typeclass

theorem loc_path_connected_of_bases {X : Type u_1} [topological_space X] {ι : Type u_3} {p : ι → Prop} {s : X → ι → set X} (h : ∀ (x : X), (nhds x).has_basis p (s x)) (h' : ∀ (x : X) (i : ι), p i → is_path_connected (s x i)) :

loc_path_connected_space X

theorem path_connected_space_iff_connected_space {X : Type u_1} [topological_space X] [loc_path_connected_space X] :

path_connected_space X ↔ 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} (h : is_open U) (hx : x ∈ U) :

(nhds x).has_basis (λ (s : set X), s ∈ nhds x ∧ is_path_connected s ∧ s ⊆ U) id

theorem loc_path_connected_of_is_open {X : Type u_1} [topological_space X] [loc_path_connected_space X] {U : set X} (h : is_open U) :

loc_path_connected_space ↥U

theorem is_open.is_connected_iff_is_path_connected {X : Type u_1} [topological_space X] [loc_path_connected_space X] {U : set X} (U_op : is_open U) :

is_path_connected U ↔ is_connected U