Path connectedness #
Main definitions #
In the file the unit interval
[0, 1] in
ℝ is denoted by
X is a topological space.
path (x y : X)is the type of paths from
y, i.e., continuous maps from
path.mapis the image of a path under a continuous map.
joined (x y : X)means there is a path between
joined.some_path (h : joined x y)selects some path between two points
path_component (x : X)is the set of points joined to
path_connected_space Xis a predicate class asserting that
Xis non-empty and every two points of
Then there are corresponding relative notions for
F : set X.
joined_in F (x y : X)means there is a path
ywith values in
joined_in.some_path (h : joined_in F x y)selects a path from
path_component_in F (x : X)is the set of points joined to
is_path_connected Fasserts that
Fis non-empty and every two points of
Fare joined in
loc_path_connected_space Xis a predicate class asserting that
Xis 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
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
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
φ : Π (a : α), path (x a) (y a) can be seen as a function
α × I → X.
The path obtained from a map defined on
ℝ by restriction to the unit interval.
Concatenation of two paths from
y and from
z, putting the first
[0, 1/2] and the second one on
Truncating a path #
γ.truncate t₀ t₁ is the path which follows the path
γ on the
[t₀, t₁] and stays still otherwise.
γ.truncate_of_le t₀ t₁ h, where
h : t₀ ≤ t₁ is
γ.truncate t₀ t₁
casted as a path from
γ.extend t₀ to
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.
Being joined by a path #
Being joined by a path inside a set #
Path component #
Path connected sets #
Path connected spaces #
Locally path connected spaces #
A topological space is locally path connected, at every point, path connected neighborhoods form a neighborhood basis.