pointReflection_self — Mathlib

English

Let P be an additive torsor over G. For any x ∈ P, the reflection about x fixes x; i.e., applying the reflection map to x yields x.

Русский

Пусть P — аддитивный торсор над G. Для любого x ∈ P отражение относительно точки x фиксирует x: отражение x отправляет x в x.

LaTeX

$$$(\mathrm{pointReflection}\, x)\, x = x$$$

Lean4

@[simp]
theorem pointReflection_self (x : P) : pointReflection x x = x :=
  vsub_vadd _ _

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