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

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