pointReflection_center_left — Mathlib

English

If s.IsDiameter p1 p2, then the point Reflection of p1 about the center equals p2.

Русский

Если s — диаметр между p1 и p2, то отражение точки p1 через центр даёт p2.

LaTeX

$$$\operatorname{pointReflection}(s.center)(p_1) = p_2$$$

Lean4

theorem pointReflection_center_left (h : s.IsDiameter p₁ p₂) : Equiv.pointReflection s.center p₁ = p₂ := by
  rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_left]

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