pointReflection_vsub_right

Mathlib.Algebra.AddTorsor.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.pointReflection_vsub_right

← MathLib Explorer

English

The left VSub under pointReflection satisfies (pointReflection x y) -ᵥ x = x -ᵥ y.

Русский

Левая VSub под точечным отражением: (pointReflection x y) -ᵥ x = x -ᵥ y.

LaTeX

$$$\text{pointReflection}(x)(y) -ᵥ x = x -ᵥ y$$$

Lean4

@[simp]
theorem pointReflection_vsub_right (x y : P) : pointReflection x y -ᵥ y = 2 • (x -ᵥ y) := by
  simp [pointReflection, two_nsmul, vadd_vsub_assoc]

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

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

Разделы

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

Аффилиация

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