pointReflection_self

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

If 2•· is injective on V1, then for any y, the map x ↦ pointReflection k x y is injective.

Русский

Если удвоение инъективно в V1, то для любого y отображение x ↦ pointReflection k x y инъективно.

LaTeX

$$Injective (2•·: V1 → V1) ⇒ Injective (x ↦ pointReflection k x y)$$

Lean4

theorem pointReflection_self (x : P₁) : pointReflection k x x = x :=
  vsub_vadd _ _

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

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

Разделы

Аффилиация

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