midpoint_sub_left

Mathlib.LinearAlgebra.AffineSpace.Midpoint

URI: https://scilib.ai/kg/mathlib#midpoint_sub_left

English

Alternative form: midpoint(R,x,y)=z iff Equiv.pointReflection(z,x)=y.

Русский

Альтернативная форма: midpoint(R,x,y)=z ⇔ Equiv.pointReflection(z,x)=y.

LaTeX

$$$ \\operatorname{midpoint}(R,x,y) = z \\iff \\operatorname{pointReflection}(z,x) = y $$$

Lean4

@[simp]
theorem midpoint_sub_left (v₁ v₂ : V) : midpoint R v₁ v₂ - v₁ = (⅟2 : R) • (v₂ - v₁) :=
  midpoint_vsub_left v₁ v₂

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

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

Разделы

Аффилиация

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