reflection_reflection — Mathlib

English

The map sending p to its reflection is an involution: applying reflection twice gives the original point.

Русский

Отображение, отправляющее p в отражение, является инволютивным: два раза применение возвращает исходную точку.

LaTeX

$$$\\text{reflection\\_involutive} : \\text{Involutive}(K.reflection)$$$

Lean4

/-- Reflecting twice in the same subspace. -/
@[simp]
theorem reflection_reflection (p : E) : K.reflection (K.reflection p) = p :=
  K.reflection.left_inv p

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