midpoint_eq_left_iff

Mathlib.LinearAlgebra.AffineSpace.Midpoint

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

English

The midpoint lies at the left vertex iff x = y, i.e., midpoint(R,x,y) = x iff x = y.

Русский

Средняя находится в левой вершине тогда и только тогда, когда x = y.

LaTeX

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

Lean4

@[simp]
theorem midpoint_eq_left_iff {x y : P} : midpoint R x y = x ↔ x = y := by rw [midpoint_eq_iff, pointReflection_self]

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

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

Разделы

Аффилиация

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