mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero

English

Let c ∈ perpBisector(p1,p2). Then the inner product ⟪ Equiv.pointReflection(c,p1) − p2, p2 − p1 ⟫ equals 0, i.e., the reflected point of c about p1, relative to p2, is orthogonal to p2 − p1.

Русский

Пусть c принадлежит perpBisector(p1,p2). Тогда ⟪ Ref_{p1}(c) − p2, p2 − p1 ⟫ = 0, где Ref_{p1}(c) — точечное отражение c через p1.

LaTeX

$$$c \in \perpBisector(p_1,p_2) \iff \langle \text{pointReflection}(c,p_1) - p_2,\; p_2 - p_1 \rangle = 0$$$

Lean4

theorem mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero :
    c ∈ perpBisector p₁ p₂ ↔ ⟪Equiv.pointReflection c p₁ -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0 :=
  by
  rw [mem_perpBisector_iff_inner_eq_zero, Equiv.pointReflection_apply, vsub_midpoint, invOf_eq_inv, ← smul_add,
    real_inner_smul_left, vadd_vsub_assoc]
  simp

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