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

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

Perpendicular bisector of a segment in a Euclidean affine space.

Equations

• AffineSubspace.perpBisector p₁ p₂ = AffineSubspace.mk' (midpoint ℝ p₁ p₂) ((innerₛₗ ℝ) (p₂ -ᵥ p₁)).ker

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} : c ∈ perpBisector p₁ p₂ ↔ inner ℝ (p₂ -ᵥ p₁) (c -ᵥ midpoint ℝ p₁ p₂) = 0

A point c belongs the perpendicular bisector of [p₁, p₂] iff p₂ -ᵥ p₁ is orthogonal to c -ᵥ 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} : c ∈ perpBisector p₁ p₂ ↔ inner ℝ (c -ᵥ midpoint ℝ p₁ p₂) (p₂ -ᵥ p₁) = 0

A point c belongs the perpendicular bisector of [p₁, p₂] iff c -ᵥ midpoint ℝ p₁ p₂ is orthogonal to p₂ -ᵥ 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} : c ∈ perpBisector p₁ p₂ ↔ inner ℝ ((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} : c ∈ perpBisector p₁ ((Equiv.pointReflection p₂) p₁) ↔ inner ℝ (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) : midpoint ℝ p₁ p₂ ∈ 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} : (↑(perpBisector p₁ p₂)).Nonempty

@[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) : (perpBisector p₁ p₂).direction = (ℝ ∙ (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} : c ∈ perpBisector p₁ p₂ ↔ inner ℝ (c -ᵥ p₁) (p₂ -ᵥ p₁) = inner ℝ (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} : c ∈ perpBisector p₁ p₂ ↔ inner ℝ (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} : c ∈ 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} : c ∈ 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) : perpBisector p₁ p₂ = 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₂ ∈ 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₁ ∈ 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) : 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} : 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} : perpBisector p₁ p₂ ≠ ⊥

theorem EuclideanGeometry.dist_lt_of_sbtw_of_inner_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c p : P} (h_sbtw : Sbtw ℝ a b c) (h_inner : inner ℝ (p -ᵥ a) (b -ᵥ a) = 0) : dist p b < dist p c

If b is strictly between a and c, and p -ᵥ a is orthogonal to b -ᵥ a, then p is closer to b than to c.

theorem EuclideanGeometry.dist_le_of_wbtw_of_inner_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c p : P} (h_wbtw : Wbtw ℝ a b c) (h_inner : inner ℝ (p -ᵥ a) (c -ᵥ a) = 0) : dist p b ≤ dist p c

If b is weakly between a and c, and p -ᵥ a is orthogonal to c -ᵥ a, then p is at least as close to b as to c.

theorem EuclideanGeometry.dist_lt_of_sbtw_of_mem_perpBisector {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c p : P} (h_sbtw : Sbtw ℝ a b c) (hp : p ∈ AffineSubspace.perpBisector a b) : dist p b < dist p c

If p lies on the perpendicular bisector of ab and b is strictly between a and c, then p is closer to b than to c.

theorem EuclideanGeometry.dist_le_of_wbtw_of_mem_perpBisector {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c p : P} (h_wbtw : Wbtw ℝ a b c) (hab : a ≠ b) (hp : p ∈ AffineSubspace.perpBisector a b) : dist p b ≤ dist p c

If p lies on the perpendicular bisector of ab and b is weakly between a and c, then p is at least as close to b as to c.

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₁ c₂ p₁ p₂ : P} (hc₁ : dist p₁ c₁ = dist p₂ c₁) (hc₂ : dist p₁ c₂ = dist p₂ c₂) : inner ℝ (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) : 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) : Set.MapsTo f ↑(AffineSubspace.perpBisector p₁ p₂) ↑(AffineSubspace.perpBisector (f p₁) (f p₂))