# Perpendicular bisector of a segment #

We define AffineSubspace.perpBisector p₁ p₂ to be the perpendicular bisector of the segment [p₁, p₂], as a bundled affine subspace. We also prove that a point belongs to the perpendicular bisector if and only if it is equidistant from p₁ and p₂, as well as a few linear equations that define this subspace.

## Keywords #

euclidean geometry, perpendicular, perpendicular bisector, line segment bisector, equidistant

def AffineSubspace.perpBisector {V : Type u_1} {P : Type u_2} [] [] [] (p₁ : P) (p₂ : P) :

Perpendicular bisector of a segment in a Euclidean affine space.

Equations
Instances For
theorem AffineSubspace.mem_perpBisector_iff_inner_eq_zero' {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {p₁ : P} {p₂ : P} :
c p₂ -ᵥ p₁, c -ᵥ midpoint p₁ p₂⟫_ = 0

A point c belongs the perpendicular bisector of [p₁, p₂] iff p₂ -ᵥ p₁is orthogonal toc -ᵥ midpoint ℝ p₁ p₂.

theorem AffineSubspace.mem_perpBisector_iff_inner_eq_zero {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {p₁ : P} {p₂ : P} :
c c -ᵥ midpoint p₁ p₂, p₂ -ᵥ p₁⟫_ = 0

A point c belongs the perpendicular bisector of [p₁, p₂] iff c -ᵥ midpoint ℝ p₁ p₂is orthogonal top₂ -ᵥ p₁.

theorem AffineSubspace.mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {p₁ : P} {p₂ : P} :
c p₁ -ᵥ p₂, p₂ -ᵥ p₁⟫_ = 0
theorem AffineSubspace.mem_perpBisector_pointReflection_iff_inner_eq_zero {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {p₁ : P} {p₂ : P} :
c AffineSubspace.perpBisector p₁ ( p₁) c -ᵥ p₂, p₁ -ᵥ p₂⟫_ = 0
theorem AffineSubspace.midpoint_mem_perpBisector {V : Type u_1} {P : Type u_2} [] [] [] (p₁ : P) (p₂ : P) :
midpoint p₁ p₂
theorem AffineSubspace.perpBisector_nonempty {V : Type u_1} {P : Type u_2} [] [] [] {p₁ : P} {p₂ : P} :
@[simp]
theorem AffineSubspace.direction_perpBisector {V : Type u_1} {P : Type u_2} [] [] [] (p₁ : P) (p₂ : P) :
= (Submodule.span {p₂ -ᵥ p₁})
theorem AffineSubspace.mem_perpBisector_iff_inner_eq_inner {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {p₁ : P} {p₂ : P} :
c c -ᵥ p₁, p₂ -ᵥ p₁⟫_ = c -ᵥ p₂, p₁ -ᵥ p₂⟫_
theorem AffineSubspace.mem_perpBisector_iff_inner_eq {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {p₁ : P} {p₂ : P} :
c c -ᵥ p₁, p₂ -ᵥ p₁⟫_ = dist p₁ p₂ ^ 2 / 2
theorem AffineSubspace.mem_perpBisector_iff_dist_eq {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {p₁ : P} {p₂ : P} :
c dist c p₁ = dist c p₂
theorem AffineSubspace.mem_perpBisector_iff_dist_eq' {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {p₁ : P} {p₂ : P} :
c dist p₁ c = dist p₂ c
theorem AffineSubspace.perpBisector_comm {V : Type u_1} {P : Type u_2} [] [] [] (p₁ : P) (p₂ : P) :
@[simp]
theorem AffineSubspace.right_mem_perpBisector {V : Type u_1} {P : Type u_2} [] [] [] {p₁ : P} {p₂ : P} :
p₂ p₁ = p₂
@[simp]
theorem AffineSubspace.left_mem_perpBisector {V : Type u_1} {P : Type u_2} [] [] [] {p₁ : P} {p₂ : P} :
p₁ p₁ = p₂
@[simp]
theorem AffineSubspace.perpBisector_self {V : Type u_1} {P : Type u_2} [] [] [] (p : P) :
@[simp]
theorem AffineSubspace.perpBisector_eq_top {V : Type u_1} {P : Type u_2} [] [] [] {p₁ : P} {p₂ : P} :
p₁ = p₂
@[simp]
theorem AffineSubspace.perpBisector_ne_bot {V : Type u_1} {P : Type u_2} [] [] [] {p₁ : P} {p₂ : P} :
theorem EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq {V : Type u_1} {P : Type u_2} [] [] [] {c₁ : P} {c₂ : P} {p₁ : P} {p₂ : P} (hc₁ : dist p₁ c₁ = dist p₂ c₁) (hc₂ : dist p₁ c₂ = dist p₂ c₂) :
c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ = 0

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 Isometry.preimage_perpBisector {V : Type u_1} {P : Type u_2} [] [] [] {V' : Type u_3} {P' : Type u_4} [] [] [] [NormedAddTorsor V' P'] {f : PP'} (h : ) (p₁ : P) (p₂ : P) :
f ⁻¹' (AffineSubspace.perpBisector (f p₁) (f p₂)) = ()
theorem Isometry.mapsTo_perpBisector {V : Type u_1} {P : Type u_2} [] [] [] {V' : Type u_3} {P' : Type u_4} [] [] [] [NormedAddTorsor V' P'] {f : PP'} (h : ) (p₁ : P) (p₂ : P) :
Set.MapsTo f () (AffineSubspace.perpBisector (f p₁) (f p₂))