affineSegment_same — Mathlib

English

If the endpoints coincide, the affine segment reduces to the single point {x}.

Русский

Если концы совпадают, афинный отрезок сводится к единственной точке {x}.

LaTeX

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

Lean4

@[simp]
theorem affineSegment_same (x : P) : affineSegment R x x = { x } := by
  simp_rw [affineSegment, lineMap_same, AffineMap.coe_const, Function.const,
    (Set.nonempty_Icc.mpr zero_le_one).image_const]

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