affineSegment_eq_segment — Mathlib

English

In a suitable vector space, the affine segment equals the (ordinary) segment: affineSegment(R, x, y) = segment(R, x, y).

Русский

При надлежащем векторном пространстве афинный отрезок равен обычному отрезку: affineSegment(R, x, y) = segment(R, x, y).

LaTeX

$$$\operatorname{affineSegment}(R,x,y) = \operatorname{segment}(R,x,y).$$$

Lean4

theorem affineSegment_eq_segment (x y : V) : affineSegment R x y = segment R x y := by
  rw [segment_eq_image_lineMap, affineSegment]

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