segment_symm — Mathlib

English

The reverse of a segment from a to b is the segment from b to a. In other words, reading the straight path from a to b backwards yields the path from b to a.

Русский

Обратная цепь сегмента от a к b равна сегменту от b к a. Иными словами, путь по прямой от a к b в обратном направлении равен пути от b к a.

LaTeX

$$$ (Path.segment\; a\; b)^{-1} = Path.segment\; b\; a $$$

Lean4

@[simp]
protected theorem segment_symm (a b : E) : (Path.segment a b).symm = .segment b a := by ext; simp

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