segment_add_segment — Mathlib

English

The sum (concatenation) of two segments equals the segment with summed endpoints: the path from a to b plus the path from c to d equals the path from a+c to b+d.

Русский

Сумма двух сегментов эквивалентна сегменту с суммированными концами: путь от a к b плюс путь от c к d равен пути от a+c к b+d.

LaTeX

$$$ (Path.segment\ a\ b) + (Path.segment\ c\ d) = Path.segment\ (a+c)\ (b+d) $$$

Lean4

@[simp]
theorem segment_add_segment (a b c d : E) : (Path.segment a b).add (.segment c d) = .segment (a + c) (b + d) :=
  by
  ext
  simp [lineMap_apply_module, add_add_add_comm]

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