# Segment between 2 points as a bundled path #

In this file we define `Path.segment a b : Path a b` to be the path going from `a` to `b` along the straight segment with constant velocity `b - a`.

We also prove basic properties of this construction, then use it to show that a nonempty convex set is path connected. In particular, a topological vector space over `ℝ` is path connected.

source
def Path.segment {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (a b : E) :
Path a b

The path from `a` to `b` going along a straight line segment

Equations

- Path.segment a b = { toFun := fun (t : ↑unitInterval) => (AffineMap.lineMap a b) ↑t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

Instances For

source
@[simp]
theorem Path.segment_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (a b : E) (t : ↑unitInterval) :
(Path.segment a b) t = (AffineMap.lineMap a b) ↑t
source
@[simp]
theorem Path.range_segment {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (a b : E) :
Set.range ⇑(Path.segment a b) = segment ℝ a b
source
@[simp]
theorem Path.segment_same {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (a : E) :
Path.segment a a = refl a
source
@[simp]
theorem Path.segment_symm {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (a b : E) :
(Path.segment a b).symm = Path.segment b a
source
@[simp]
theorem Path.segment_add_segment {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (a b c d : E) :
(Path.segment a b).add (Path.segment c d) = Path.segment (a + c) (b + d)
source
@[simp]
theorem Path.cast_segment {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {a b c d : E} (hac : c = a) (hbd : d = b) :
(Path.segment a b).cast hac hbd = Path.segment c d
source
theorem Path.eqOn_extend_segment {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (a b : E) :
Set.EqOn (⇑(Path.segment a b).extend) (⇑(AffineMap.lineMap a b)) unitInterval
source
theorem JoinedIn.of_segment_subset {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {x y : E} {s : Set E} (h : segment ℝ x y ⊆ s) :
JoinedIn s x y
source
theorem StarConvex.isPathConnected {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {s : Set E} {a : E} (h : StarConvex ℝ a s) (ha : a ∈ s) :
IsPathConnected s
source
theorem Convex.isPathConnected {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {s : Set E} (hconv : Convex ℝ s) (hne : s.Nonempty) :
IsPathConnected s

A nonempty convex set is path connected.

source
theorem Convex.isConnected {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {s : Set E} (h : Convex ℝ s) (hne : s.Nonempty) :
IsConnected s

A nonempty convex set is connected.

source
theorem Convex.isPreconnected {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {s : Set E} (h : Convex ℝ s) :
IsPreconnected s

A convex set is preconnected.

source
theorem Submodule.isPathConnected {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (s : Submodule ℝ E) :
IsPathConnected ↑s

A subspace in a topological vector space over `ℝ` is path connected.

source
theorem IsTopologicalAddGroup.pathConnectedSpace {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] :
PathConnectedSpace E

Every topological vector space over ℝ is path connected.

Not an instance, because it creates enormous TC subproblems (turn on `pp.all`).

source
theorem isPathConnected_compl_of_isPathConnected_compl_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {p q : Submodule ℝ E} (hpq : IsCompl p q) (hpc : IsPathConnected {0}ᶜ) :
IsPathConnected (↑q)ᶜ

Given two complementary subspaces `p` and `q` in `E`, if the complement of `{0}` is path connected in `p` then the complement of `q` is path connected in `E`.