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 fromxtoy, i.e., continuous maps fromItoXmapping0toxand1toy.path.mapis the image of a path under a continuous map.joined (x y : X)means there is a path betweenxandy.joined.some_path (h : joined x y)selects some path between two pointsxandy.path_component (x : X)is the set of points joined tox.path_connected_space Xis a predicate class asserting thatXis non-empty and every two points ofXare joined.
Then there are corresponding relative notions for F : set X.
joined_in F (x y : X)means there is a pathγjoiningxtoywith values inF.joined_in.some_path (h : joined_in F x y)selects a path fromxtoyinsideF.path_component_in F (x : X)is the set of points joined toxinF.is_path_connected Fasserts thatFis non-empty and every two points ofFare joined inF.loc_path_connected_space Xis a predicate class asserting thatXis locally path-connected: each point has a basis of path-connected neighborhoods (we do not ask these to be open).
Main theorems
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 Xis_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 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
Equations
- I_has_zero = {zero := ⟨0, I_has_zero._proof_1⟩}
Equations
Equations
Paths
Equations
- path.has_coe_to_fun = {F := λ (x : path x y), ↥(set.Icc 0 1) → X, coe := path.to_fun y}
The constant path from a point to itself
The reverse of a path from x to y, as a path from y to x
A continuous map extending a path to ℝ, constant before 0 and after 1.
The path obtained from a map defined on ℝ by restriction to the unit interval.
Equations
- path.of_line hf h₀ h₁ = {to_fun := f ∘ coe, continuous' := _, source' := h₀, target' := h₁}
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].
Image of a path from x to y by a continuous map
Casting a path from x to y to a path from x' to y' when x' = x and y' = y
Being joined by a path
When two points are joined, choose some path from x to y.
Equations
- h.some_path = nonempty.some h
The setoid corresponding the equivalence relation of being joined by a continuous path.
The quotient type of points of a topological space modulo being joined by a continuous path.
Equations
- zeroth_homotopy X = quotient (path_setoid X)
Being joined by a path inside a set
When x and y are joined in F, choose a path from x to y inside F
Equations
- h.some_path = classical.some h
If x and y are joined in the set F, then they are joined in the subtype F.
Path component
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}
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}
Path connected sets
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
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).
Path connected spaces
A topological space is path-connected if it is non-empty and every two points can be joined by a continuous path.
Instances
Use path-connectedness to build a path between two points.