mem_perpBisector_pointReflection_iff_inner_eq_zero

English

Let c ∈ perpBisector(p1, Ref(p2,p1)). Then ⟪ c − p2, p1 − p2 ⟫ = 0.

Русский

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

LaTeX

$$$c \in \perpBisector(p_1, \mathrm{Ref}(p_2,p_1)) \iff \langle c - p_2, p_1 - p_2 \rangle = 0$$$

Lean4

theorem mem_perpBisector_pointReflection_iff_inner_eq_zero :
    c ∈ perpBisector p₁ (Equiv.pointReflection p₂ p₁) ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0 := by
  rw [mem_perpBisector_iff_inner_eq_zero, midpoint_pointReflection_right, Equiv.pointReflection_apply, vadd_vsub_assoc,
    inner_add_right, add_self_eq_zero, ← neg_eq_zero, ← inner_neg_right, neg_vsub_eq_vsub_rev]

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