inner_vsub_vsub_of_dist_eq_of_dist_eq

English

If c1 and c2 are equidistant to p1 and p2, then (c2 − c1) is orthogonal to (p2 − p1).

Русский

Если c1 и c2 равноудалены от p1 и p2, то (c2 − c1) ортогонален (p2 − p1).

LaTeX

$$$\langle c_2 - c_1, p_2 - p_1 \rangle = 0$ under the given distance equalities$$

Lean4

/-- Suppose that `c₁` is equidistant from `p₁` and `p₂`, and the same applies to `c₂`. Then the
vector between `c₁` and `c₂` is orthogonal to that between `p₁` and `p₂`. (In two dimensions, this
says that the diagonals of a kite are orthogonal.) -/
theorem inner_vsub_vsub_of_dist_eq_of_dist_eq {c₁ c₂ p₁ p₂ : P} (hc₁ : dist p₁ c₁ = dist p₂ c₁)
    (hc₂ : dist p₁ c₂ = dist p₂ c₂) : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 :=
  by
  rw [← Submodule.mem_orthogonal_singleton_iff_inner_left, ← direction_perpBisector]
  apply vsub_mem_direction <;> rwa [mem_perpBisector_iff_dist_eq']

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