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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) : AffineSubspace ℝ P

Perpendicular bisector of a segment in a Euclidean affine space.

Equations

• AffineSubspace.perpBisector p₁ p₂ = AffineSubspace.comap (↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (midpoint ℝ p₁ p₂)))) (Submodule.toAffineSubspace (LinearMap.ker ((innerₛₗ ℝ) (p₂ -ᵥ p₁))))

theorem AffineSubspace.mem_perpBisector_iff_inner_eq_zero' {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {p₁ : P} {p₂ : P} : c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {p₁ : P} {p₂ : P} : c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {p₁ : P} {p₂ : P} : c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪(Equiv.pointReflection c) p₁ -ᵥ p₂, p₂ -ᵥ p₁⟫_ℝ = 0

theorem AffineSubspace.mem_perpBisector_pointReflection_iff_inner_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {p₁ : P} {p₂ : P} : c ∈ AffineSubspace.perpBisector p₁ ((Equiv.pointReflection p₂) p₁) ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ = 0

theorem AffineSubspace.midpoint_mem_perpBisector {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) : midpoint ℝ p₁ p₂ ∈ AffineSubspace.perpBisector p₁ p₂

theorem AffineSubspace.perpBisector_nonempty {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} : Set.Nonempty ↑(AffineSubspace.perpBisector p₁ p₂)

@[simp]

theorem AffineSubspace.direction_perpBisector {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) : AffineSubspace.direction (AffineSubspace.perpBisector p₁ p₂) = (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ

theorem AffineSubspace.mem_perpBisector_iff_inner_eq_inner {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {p₁ : P} {p₂ : P} : c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ

theorem AffineSubspace.mem_perpBisector_iff_inner_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {p₁ : P} {p₂ : P} : c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ = dist p₁ p₂ ^ 2 / 2

theorem AffineSubspace.mem_perpBisector_iff_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {p₁ : P} {p₂ : P} : c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ dist c p₁ = dist c p₂

theorem AffineSubspace.mem_perpBisector_iff_dist_eq' {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {p₁ : P} {p₂ : P} : c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ dist p₁ c = dist p₂ c

theorem AffineSubspace.perpBisector_comm {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) : AffineSubspace.perpBisector p₁ p₂ = AffineSubspace.perpBisector p₂ p₁

@[simp]

theorem AffineSubspace.right_mem_perpBisector {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} : p₂ ∈ AffineSubspace.perpBisector p₁ p₂ ↔ p₁ = p₂

@[simp]

theorem AffineSubspace.left_mem_perpBisector {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} : p₁ ∈ AffineSubspace.perpBisector p₁ p₂ ↔ p₁ = p₂

@[simp]

theorem AffineSubspace.perpBisector_self {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p : P) : AffineSubspace.perpBisector p p = ⊤

@[simp]

theorem AffineSubspace.perpBisector_eq_top {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} : AffineSubspace.perpBisector p₁ p₂ = ⊤ ↔ p₁ = p₂

@[simp]

theorem AffineSubspace.perpBisector_ne_bot {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} : AffineSubspace.perpBisector p₁ p₂ ≠ ⊥

theorem EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V' : Type u_3} {P' : Type u_4} [NormedAddCommGroup V'] [InnerProductSpace ℝ V'] [MetricSpace P'] [NormedAddTorsor V' P'] {f : P → P'} (h : Isometry f) (p₁ : P) (p₂ : P) : f ⁻¹' ↑(AffineSubspace.perpBisector (f p₁) (f p₂)) = ↑(AffineSubspace.perpBisector p₁ p₂)

theorem Isometry.mapsTo_perpBisector {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V' : Type u_3} {P' : Type u_4} [NormedAddCommGroup V'] [InnerProductSpace ℝ V'] [MetricSpace P'] [NormedAddTorsor V' P'] {f : P → P'} (h : Isometry f) (p₁ : P) (p₂ : P) : Set.MapsTo f ↑(AffineSubspace.perpBisector p₁ p₂) ↑(AffineSubspace.perpBisector (f p₁) (f p₂))