pointReflection_midpoint_right — Mathlib

English

Reflecting about the midpoint of x and y with center at Real yields the swap of x and y: pointReflection Real (midpoint Real x y) x = y.

Русский

Отражение через середину между x и y с центром Real отправляет x в y: pointReflection Real (midpoint Real x y) x = y.

LaTeX

$$$\operatorname{pointReflection}_{\mathbb{R}}(\tfrac{x+y}{2})\, x = y$$$

Lean4

@[simp]
theorem pointReflection_midpoint_right (x y : P) : pointReflection ℝ (midpoint ℝ x y) y = x :=
  AffineEquiv.pointReflection_midpoint_right x y

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