midpoint_add_sub

Mathlib.LinearAlgebra.AffineSpace.Midpoint

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

English

Similarly, the midpoint of x + y and x − y is x.

Русский

Аналогично, середина между x + y и x − y равна x.

LaTeX

$$$ \operatorname{midpoint} R (x + y) (x - y) = x $$$

Lean4

@[simp]
theorem midpoint_add_sub (x y : V) : midpoint R (x + y) (x - y) = x := by rw [midpoint_comm]; simp

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

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

Разделы

Аффилиация

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