mem_perpBisector_iff_dist_eq — Mathlib

English

Same as previous: c ∈ perpBisector(p1,p2) iff dist p1 c = dist p2 c.

Русский

То же, что и ранее: c ∈ perpBisector(p1,p2) тогда и только тогда, когда dist(p1,c) = dist(p2,c).

LaTeX

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

Lean4

theorem mem_perpBisector_iff_dist_eq : c ∈ perpBisector p₁ p₂ ↔ dist c p₁ = dist c p₂ := by
  rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff, vsub_sub_vsub_cancel_left,
    inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right, neg_vsub_eq_vsub_rev,
    mem_perpBisector_iff_inner_eq_inner]

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