midpoint_eq_iff'

Mathlib.LinearAlgebra.AffineSpace.Midpoint

URI: https://scilib.ai/kg/mathlib#midpoint_eq_iff'

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

theorem midpoint_eq_iff' {x y z : P} : midpoint R x y = z ↔ Equiv.pointReflection z x = y :=
  midpoint_eq_iff

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

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

Разделы

Аффилиация

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