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
- 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
y in a topological space
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
φ : Π (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
Image of a path from
y by a continuous map
Casting a path from
y to a path from
x' = x and
y' = y
Product of paths #
Given a path in
X and a path in
Y, we can take their pointwise product to get a path in
X × Y.
Path composition commutes with products
Given a family of paths, one in each Xᵢ, we take their pointwise product to get a path in Π i, Xᵢ.
Path composition commutes with products
Pointwise multiplication/addition of two paths in a topological (additive) group #
Pointwise addition of paths in a topological additive group.
Pointwise multiplication of paths in a topological group. The additive version is probably more useful.
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.
Reparametrising a path #
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.
Being joined by a path #
Being joined by a path inside a set #
Path component #
Path connected sets #
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.
Locally path connected spaces #
- 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.