Mathlib.Geometry.Euclidean.PerpBisector._auxLemma.2
theorem Mathlib.Geometry.Euclidean.PerpBisector._auxLemma.2 :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P},
(c ∈ AffineSubspace.perpBisector p₁ p₂) = (dist c p₁ = dist c p₂)
The theorem `Mathlib.Geometry.Euclidean.PerpBisector._auxLemma.2` states that for any types `V` and `P`, where `V` is a normed additive commutative group, `P` is a metric space, and `V` acts on `P` normed additively, and for any points `c`, `p₁`, and `p₂` in `P`, `c` is in the perpendicular bisector of the segment `p₁ p₂` if and only if the distance from `c` to `p₁` is equal to the distance from `c` to `p₂`. In other words, the perpendicular bisector of a line segment is the set of all points that are equidistant from the endpoints of the line segment.
More concisely: A point is on the perpendicular bisector of a line segment if and only if it has equal distance to both segment endpoints.
|
EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq
theorem EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {c₁ c₂ p₁ p₂ : P},
dist p₁ c₁ = dist p₂ c₁ → dist p₁ c₂ = dist p₂ c₂ → ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0
This theorem states that in an inner product space over the reals, with a corresponding metric space and normed add torsor, if two points `c₁` and `c₂` are each equidistant from two other points `p₁` and `p₂` (that is, the distance from `p₁` to `c₁` equals the distance from `p₂` to `c₁` and the distance from `p₁` to `c₂` equals the distance from `p₂` to `c₂`), then the inner product of the vector from `c₁` to `c₂` and the vector from `p₁` to `p₂` is zero. In other words, these vectors are orthogonal. An intuitive example in two dimensions is that the diagonals of a kite are always orthogonal.
More concisely: In an inner product space over the reals, if points `c₁` and `c₂` are equidistant from points `p₁` and `p₂`, then the vector from `c₁` to `c₂` is orthogonal to the vector from `p₁` to `p₂` (i.e., their inner product is zero).
|
AffineSubspace.mem_perpBisector_iff_inner_eq_zero'
theorem AffineSubspace.mem_perpBisector_iff_inner_eq_zero' :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P},
c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪p₂ -ᵥ p₁, c -ᵥ midpoint ℝ p₁ p₂⟫_ℝ = 0
The theorem `AffineSubspace.mem_perpBisector_iff_inner_eq_zero'` states that for any points `c`, `p₁`, and `p₂` in a Euclidean affine space with a metric and an inner product, the point `c` lies on the perpendicular bisector of the line segment `[p₁, p₂]` if and only if the vector from `p₁` to `p₂` (`p₂ -ᵥ p₁`) is orthogonal to the vector from `c` to the midpoint of `p₁` and `p₂` (`c -ᵥ midpoint ℝ p₁ p₂`). Here, orthogonality is determined by the inner product of the two vectors being equal to zero (`⟪p₂ -ᵥ p₁, c -ᵥ midpoint ℝ p₁ p₂⟫_ℝ = 0`).
More concisely: A point c in a Euclidean affine space is on the perpendicular bisector of the line segment [p₁, p₂] if and only if the inner product of the vector from p₁ to p₂ and the vector from c to the midpoint of p₁ and p₂ is zero.
|
AffineSubspace.mem_perpBisector_iff_inner_eq_zero
theorem AffineSubspace.mem_perpBisector_iff_inner_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P},
c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫_ℝ = 0
The theorem `AffineSubspace.mem_perpBisector_iff_inner_eq_zero` states that for a given point `c` and a segment defined by points `p₁` and `p₂` in a Euclidean affine space, `c` lies on the perpendicular bisector of the segment `[p₁, p₂]` if and only if the vector formed by `c` and the midpoint of `p₁` and `p₂` is orthogonal (i.e., the inner product equals zero) to the vector formed by `p₂` and `p₁`. This theorem provides a condition related to inner products for checking if a point is on the perpendicular bisector of a given segment.
More concisely: A point c in a Euclidean affine space is on the perpendicular bisector of the segment [p₁, p₂] if and only if the vector from c to the midpoint of p₁ and p₂ is orthogonal to the vector from p₁ to p₂. (Equivalently, the inner product of these two vectors is zero.)
|