segment — Mathlib

English

The segment from a to b in a vector space E is the straight line Path a b parameterized by t ↦ lineMap a b t, giving a path between a and b.

Русский

Сегмент от a к b в векторном пространстве E задаёт путь по прямой линии: t ↦ lineMap a b t, соединяющий a и b.

LaTeX

$$$\text{Path.segment}(a,b) : \text{Path } a b$$$

Lean4

/-- The path from `a` to `b` going along a straight line segment -/
@[simps]
protected def segment (a b : E) : Path a b
    where
  toFun t := lineMap a b (t : ℝ)
  source' := by simp
  target' := by simp

Похожие утверждения