Documentation

Mathlib.Geometry.Euclidean.PerpBisector

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

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} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {p₁ : P} {p₂ : P} :
    c AffineSubspace.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} {p₂ : P} :
    c AffineSubspace.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 top₂ -ᵥ 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} :
    (↑(AffineSubspace.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₂ : P) :
    (AffineSubspace.perpBisector p₁ p₂).direction = (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₂ 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} {p₂ : P} :
    c AffineSubspace.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} {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
    @[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_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 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₂) :
    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 : PP'} (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 : PP'} (h : Isometry f) (p₁ : P) (p₂ : P) :