left_vsub_pointReflection

Mathlib.Algebra.AddTorsor.Basic

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

English

For x, y ∈ P, x −ᵥ pointReflection x y = y −ᵥ x.

Русский

Для x, y ∈ P верно x −ᵥ pointReflection x y = y −ᵥ x.

LaTeX

$$$$ x -_{v} \\text{pointReflection } x y = y -_{v} x $$$$

Lean4

@[simp]
theorem left_vsub_pointReflection (x y : P) : x -ᵥ pointReflection x y = y -ᵥ x :=
  neg_injective <| by simp

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

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

Разделы

Аффилиация

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