mem_perpBisector_iff_inner_eq_inner

English

For c ∈ perpBisector(p1,p2), ⟪c−p1, p2−p1⟫ = ⟪c−p2, p1−p2⟫.

Русский

Для c в perpBisector(p1,p2) выполняется ⟪c−p1, p2−p1⟫ = ⟪c−p2, p1−p2⟫.

LaTeX

$$$c \in \perpBisector(p_1,p_2) \iff \langle c - p_1, p_2 - p_1 \rangle = \langle c - p_2, p_1 - p_2 \rangle$$$

Lean4

theorem mem_perpBisector_iff_inner_eq_inner : c ∈ perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ := by
  rw [Iff.comm, mem_perpBisector_iff_inner_eq_zero, ← add_neg_eq_zero, ← inner_neg_right, neg_vsub_eq_vsub_rev, ←
    inner_add_left, vsub_midpoint, invOf_eq_inv, ← smul_add, real_inner_smul_left];
  simp

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