mem_perpBisector_iff_inner_eq — Mathlib

English

A point c lies on perpBisector(p1,p2) iff dist(c,p1) = dist(c,p2).

Русский

Точка c принадлежит perpBisector(p1,p2) тогда и только тогда, когда расстояния от c до p1 и до p2 равны.

LaTeX

$$$c \in \perpBisector(p_1,p_2) \iff \operatorname{dist}(c,p_1) = \operatorname{dist}(c,p_2)$$$

Lean4

theorem mem_perpBisector_iff_inner_eq : c ∈ perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = (dist p₁ p₂) ^ 2 / 2 := by
  rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left, sub_eq_zero,
    midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq, dist_eq_norm_vsub' V,
    div_eq_inv_mul]

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