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 fromx
toy
, i.e., continuous maps fromI
toX
mapping0
tox
and1
toy
.Path.map
is the image of a path under a continuous map.Joined (x y : X)
means there is a path betweenx
andy
.Joined.somePath (h : Joined x y)
selects some path between two pointsx
andy
.pathComponent (x : X)
is the set of points joined tox
.PathConnectedSpace X
is a predicate class asserting thatX
is non-empty and every two points ofX
are joined.
Then there are corresponding relative notions for F : Set X
.
JoinedIn F (x y : X)
means there is a pathγ
joiningx
toy
with values inF
.JoinedIn.somePath (h : JoinedIn F x y)
selects a path fromx
toy
insideF
.pathComponentIn F (x : X)
is the set of points joined tox
inF
.IsPathConnected F
asserts thatF
is non-empty and every two points ofF
are joined inF
.LocPathConnectedSpace X
is a predicate class asserting thatX
is 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
.
pathConnectedSpace_iff_univ : PathConnectedSpace X ↔ IsPathConnected (univ : Set X)
isPathConnected_iff_pathConnectedSpace : IsPathConnected F ↔ PathConnectedSpace ↥F
For locally path connected spaces, we have
pathConnectedSpace_iff_connectedSpace : PathConnectedSpace X ↔ ConnectedSpace X
IsOpen.isConnected_iff_isPathConnected (U_op : IsOpen U) : IsPathConnected U ↔ IsConnected U
Implementation notes #
By default, all paths have I
as their source and X
as their target, but there is an
operation Set.IccExtend
that will extend any continuous map γ : I → X
into a continuous map
IccExtend 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 #
Continuous path connecting two points x
and y
in a topological space
- toFun : ↑unitInterval → X
- continuous_toFun : Continuous self.toFun
- source' : self.toFun 0 = x
The start point of a
Path
. - target' : self.toFun 1 = y
The end point of a
Path
.
Instances For
The start point of a Path
.
The end point of a Path
.
Equations
- ⋯ = ⋯
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 γ = ⇑γ
Instances For
Any function φ : Π (a : α), Path (x a) (y a)
can be seen as a function α × I → X
.
Equations
- Path.hasUncurryPath = { uncurry := fun (φ : (a : α) → Path (x a) (y a)) (p : α × ↑unitInterval) => (φ p.1) p.2 }
The constant path from a point to itself
Equations
- Path.refl x = { toFun := fun (_t : ↑unitInterval) => x, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
Instances For
The reverse of a path from x
to y
, as a path from y
to x
Equations
- γ.symm = { toFun := ⇑γ ∘ unitInterval.symm, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
Instances For
Space of paths #
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.topologicalSpace = TopologicalSpace.induced toContinuousMap ContinuousMap.compactOpen
A continuous map extending a path to ℝ
, constant before 0
and after 1
.
Equations
- γ.extend = Set.IccExtend Path.extend.proof_1 ⇑γ
Instances For
See Note [continuity lemma statement].
A useful special case of Continuous.path_extend
.
The path obtained from a map defined on ℝ
by restriction to the unit interval.
Equations
- Path.ofLine hf h₀ h₁ = { toFun := f ∘ Subtype.val, continuous_toFun := ⋯, source' := h₀, target' := h₁ }
Instances For
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
Instances For
Image of a path from x
to y
by a map which is continuous on the path.
Instances For
Image of a path from x
to y
by a continuous map
Equations
- γ.map h = γ.map' ⋯
Instances For
Casting a path from x
to y
to a path from x'
to y'
when x' = x
and y' = y
Equations
- γ.cast hx hy = { toFun := ⇑γ, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
Instances For
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
.
Equations
- γ₁.prod γ₂ = { toContinuousMap := γ₁.prodMk γ₂.toContinuousMap, source' := ⋯, target' := ⋯ }
Instances For
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ᵢ.
Equations
- Path.pi γ = { toContinuousMap := ContinuousMap.pi fun (i : ι) => (γ i).toContinuousMap, source' := ⋯, target' := ⋯ }
Instances For
Path composition commutes with products
Pointwise multiplication/addition of two paths in a topological (additive) group #
Pointwise multiplication of paths in a topological group. The additive version is probably more useful.
Equations
- γ₁.mul γ₂ = (γ₁.prod γ₂).map ⋯
Instances For
Truncating a path #
γ.truncate t₀ t₁
is the path which follows the path γ
on the
time interval [t₀, t₁]
and stays still otherwise.
Equations
- γ.truncate t₀ t₁ = { toFun := fun (s : ↑unitInterval) => γ.extend (min (max (↑s) t₀) t₁), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
Instances For
γ.truncateOfLE t₀ t₁ h
, where h : t₀ ≤ t₁
is γ.truncate t₀ t₁
casted as a path from γ.extend t₀
to γ.extend t₁
.
Equations
- γ.truncateOfLE h = (γ.truncate t₀ t₁).cast ⋯ ⋯
Instances For
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
.
Equations
Instances For
Being joined by a path #
When two points are joined, choose some path from x
to y
.
Equations
- h.somePath = Nonempty.some h
Instances For
The setoid corresponding the equivalence relation of being joined by a continuous path.
Equations
- pathSetoid X = { r := Joined, iseqv := ⋯ }
Instances For
The quotient type of points of a topological space modulo being joined by a continuous path.
Equations
- ZerothHomotopy X = Quotient (pathSetoid X)
Instances For
Equations
- ZerothHomotopy.inhabited = { default := Quotient.mk' 0 }
Being joined by a path inside a set #
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
- JoinedIn F x y = ∃ (γ : Path x y), ∀ (t : ↑unitInterval), γ t ∈ F
Instances For
When x
and y
are joined in F
, choose a path from x
to y
inside F
Equations
- h.somePath = Classical.choose h
Instances For
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
- pathComponent x = {y : X | Joined x y}
Instances For
The path component of x
in F
is the set of points that can be joined to x
in F
.
Equations
- pathComponentIn x F = {y : X | JoinedIn F x y}
Instances For
Path connected sets #
A set F
is path connected if it contains a point that can be joined to all other in F
.
Equations
- IsPathConnected F = ∃ x ∈ F, ∀ {y : X}, y ∈ F → JoinedIn F x y
Instances For
If f
is continuous on F
and F
is path-connected, so is f(F)
.
If f
is continuous and F
is path-connected, so is f(F)
.
If f : X → Y
is a Inducing
, f(F)
is path-connected iff F
is.
If h : X → Y
is a homeomorphism, h(s)
is path-connected iff s
is.
If h : X → Y
is a homeomorphism, h⁻¹(s)
is path-connected iff s
is.
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 path-connected space must be nonempty.
Any two points in a path-connected space must be joined by a continuous path.
Use path-connectedness to build a path between two points.
Equations
Instances For
Equations
- ⋯ = ⋯
This is a special case of NormedSpace.instPathConnectedSpace
(and
TopologicalAddGroup.pathConnectedSpace
). It exists only to simplify dependencies.
Equations
Equations
- ⋯ = ⋯
Locally path connected spaces #
A topological space is locally path connected, at every point, path connected neighborhoods form a neighborhood basis.
- path_connected_basis : ∀ (x : X), (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ IsPathConnected s) id
Each neighborhood filter has a basis of path-connected neighborhoods.
Instances
Each neighborhood filter has a basis of path-connected neighborhoods.