Theorems · Definition · general topology

Path.segment

{E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : Module ℝ E] →
      [inst_2 : TopologicalSpace E] → [ContinuousAdd E] → [ContinuousSMul ℝ E] → (a b : E) → Path a b

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

Defined in

Mathlib.Analysis.Convex.PathConnected

Cited by

31 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModuleTopologicalSpaceContinuousAddContinuousSMul