pointReflection_symm

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

URI: https://scilib.ai/kg/mathlib#AffineEquiv.pointReflection_symm

← MathLib Explorer

English

The inverse of the point reflection is itself.

Русский

Обратное точечного отражения является самим отражением.

LaTeX

$$(pointReflection(k,x)).symm = pointReflection(k,x)$$

Lean4

@[simp]
theorem pointReflection_symm (x : P₁) : (pointReflection k x).symm = pointReflection k x :=
  toEquiv_injective <| Equiv.pointReflection_symm x

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru