pointReflection_self — Mathlib

English

For any point x in P, reflecting x about itself leaves x fixed: the point reflection with center x fixes x.

Русский

Пусть точка отражения с центром x действует на x; тогда x отображается в x. Точка отражения fix.

LaTeX

$$$\operatorname{pointReflection}_{\mathbb{k}}(x)(x) = x$$$

Lean4

@[simp]
theorem pointReflection_self (x : P) : pointReflection 𝕜 x x = x :=
  AffineEquiv.pointReflection_self 𝕜 x

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