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
๐Ÿ”ธ coverage
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

Instances For
    source
    ๐Ÿ“ coverage
    @[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
    ๐Ÿ“ coverage
    @[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
    ๐Ÿ“ coverage
    @[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
    ๐Ÿ“ coverage
    @[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
    ๐Ÿ“ coverage
    @[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
    ๐Ÿ“ coverage
    @[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
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    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.