Documentation

Mathlib.Analysis.Convex.PathConnected

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
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.