EuclideanGeometry.orthogonalProjection_eq_self_iff
theorem EuclideanGeometry.orthogonalProjection_eq_self_iff :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p : P},
↑((EuclideanGeometry.orthogonalProjection s) p) = p ↔ p ∈ s
The theorem `EuclideanGeometry.orthogonalProjection_eq_self_iff` states that for any point `p` in a normed add torsor over an inner product space, the orthogonal projection of that point onto a given affine subspace `s` is equal to the point itself if and only if the point `p` lies in the subspace `s`.
More concisely: A point in a normed add torsor over an inner product space is the orthogonal projection of itself onto an affine subspace if and only if it lies in that subspace.
|
EuclideanGeometry.inter_eq_singleton_orthogonalProjectionFn
theorem EuclideanGeometry.inter_eq_singleton_orthogonalProjectionFn :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
↑s ∩ ↑(AffineSubspace.mk' p s.direction.orthogonal) = {EuclideanGeometry.orthogonalProjectionFn s p}
This theorem in Euclidean geometry states that for any point `p` in a metric space `P` equipped with an inner product space `V`, the intersection of an affine subspace `s` and the orthogonal subspace through the point `p` is a singleton set containing only the orthogonal projection of the point `p` onto the subspace `s`. This is true when the space `V` is a normed add-commutative group, `P` is a metric space, and `s` is a nonempty affine subspace of `P` that has an orthogonal projection onto `s`. The theorem is primarily used in setting up the bundled version and should not be used once that is defined.
More concisely: Given a metric space `P` with an inner product space `V`, any point `p` in a nonempty affine subspace `s` of `P` has a unique point of intersection with the orthogonal subspace of `s` passing through `p`, which is the orthogonal projection of `p` onto `s`.
|
EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_not_mem
theorem EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_not_mem :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p : P},
p ∉ s → dist p ↑((EuclideanGeometry.orthogonalProjection s) p) ≠ 0
The theorem `EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_not_mem` states that for any point `p` not lying in a given affine subspace `s` (in a Euclidean setting with the necessary structures of normed add commutative group, inner product space, metric space and normed add torsor), the distance between the point `p` and its orthogonal projection onto the subspace `s` is not zero. This is essentially the mathematical way of saying that if a point is not on a certain subspace, then it's a certain positive distance away from that subspace along the orthogonal (perpendicular) direction.
More concisely: If a point lies outside an affine subspace in a Euclidean setting, then its orthogonal projection onto the subspace is non-zero.
|
EuclideanGeometry.reflection_reflection
theorem EuclideanGeometry.reflection_reflection :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
(EuclideanGeometry.reflection s) ((EuclideanGeometry.reflection s) p) = p
This theorem, titled "Reflecting twice in the same subspace," states that for any real affine subspace `s` and any point `p`, reflecting `p` twice in the subspace `s` results in the original point `p`. Here, reflection refers to the operation in Euclidean geometry where a point is mapped to another point such that if a line is drawn from the original point to its image, that line passes through the subspace and forms equal angles with it. For this theorem to hold, the subspace `s` must be nonempty and have an orthogonal projection.
More concisely: For any real affine subspace and point, reflecting the point twice in the subspace results in the original point if the subspace is nonempty and has an orthogonal projection.
|
EuclideanGeometry.reflection_involutive
theorem EuclideanGeometry.reflection_involutive :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction], Function.Involutive ⇑(EuclideanGeometry.reflection s)
This theorem, titled "Reflection is involutive", states that in any Euclidean geometry, the reflection operation is involutive. Specifically, for any vector space `V`, any metric space `P`, given that `V` is a normed add commutative group, `V` is a real inner product space, `P` is also a normed add torsor over `V`, and given a nonempty affine subspace `s` of `P` with a defined orthogonal projection, the reflection in the affine subspace `s` is an operation that, when applied twice, returns the original element. This means that for any point, reflecting it twice across the same subspace results in the original point.
More concisely: In Euclidean geometry, the reflection operation in an affine subspace is involutive, i.e., applying it twice to any point results in the original point.
|
EuclideanGeometry.vsub_orthogonalProjection_mem_direction
theorem EuclideanGeometry.vsub_orthogonalProjection_mem_direction :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p1 : P} (p2 : P) (hp1 : p1 ∈ s),
↑(⟨p1, hp1⟩ -ᵥ (EuclideanGeometry.orthogonalProjection s) p2) ∈ s.direction
This theorem states that for any given subspace 's' of ℝ^n, if we take any point 'p1' in this subspace and another point 'p2' in ℝ^n, then the vector obtained by subtracting the orthogonal projection of 'p2' on 's' from 'p1' lies in the direction of the subspace 's'. This result applies in the context of a normed add commutative group, an inner product space, a metric space, and a normed add torsor. The subspace 's' is assumed to be nonempty and to possess an orthogonal projection.
More concisely: For any subspace $s$ of $\mathbb{R}^n$ and points $p\_1, p\_2 \in \mathbb{R}^n$, the vector $(p\_1 - \pi\_{s}(p\_2))$, where $\pi\_s$ is the orthogonal projection onto $s$, lies in the subspace $s$.
|
EuclideanGeometry.orthogonalProjectionFn_mem
theorem EuclideanGeometry.orthogonalProjectionFn_mem :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P), EuclideanGeometry.orthogonalProjectionFn s p ∈ s
This theorem states that for any point `p` in a normed add torsor over a real inner product space, the orthogonal projection of `p` onto a nonempty affine subspace `s` always belongs to `s`. In other words, when we orthogonally project a point onto a subspace, the projected point will always be contained within the same subspace. This theorem is primarily used for setting up a version of the theorem that is bundled with additional context and should not be used independently once the bundled version is defined.
More concisely: For any point in a normed add torsor over a real inner product space and any nonempty affine subspace, the orthogonal projection of the point onto the subspace lies within the subspace.
|
EuclideanGeometry.inter_eq_singleton_orthogonalProjection
theorem EuclideanGeometry.inter_eq_singleton_orthogonalProjection :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
↑s ∩ ↑(AffineSubspace.mk' p s.direction.orthogonal) = {↑((EuclideanGeometry.orthogonalProjection s) p)}
This theorem asserts that in a real inner product space endowed with a metric and a normed add torsor structure, for any affine subspace `s` with a defined orthogonal projection, the intersection of `s` and the orthogonal subspace constructed from a given point `p` and the orthogonal direction to `s` is a singleton set. Specifically, this singleton set contains the orthogonal projection of the point `p` onto the subspace `s`.
More concisely: In a real inner product space with a metric and a normed add torsor structure, for any affine subspace endowed with an orthogonal projection, the intersection of the subspace and the orthogonal subspace determined by a point and its orthogonal direction contains exactly the orthogonal projection of that point onto the subspace.
|
EuclideanGeometry.orthogonalProjection_mem_orthogonal
theorem EuclideanGeometry.orthogonalProjection_mem_orthogonal :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
↑((EuclideanGeometry.orthogonalProjection s) p) ∈ AffineSubspace.mk' p s.direction.orthogonal
The theorem `EuclideanGeometry.orthogonalProjection_mem_orthogonal` states that for any vector space `V` with an inner product, a metric space `P`, an affine torsor `V P`, a nonempty affine subspace `s` of `P`, and any point `p` in `P`, the orthogonal projection of `p` onto `s` lies in the orthogonal affine subspace constructed with the direction of `s` and `p` as a base point. In other words, it asserts that the orthogonal projection of a point onto a subspace resides in the orthogonal subspace of that original subspace.
More concisely: The orthogonal projection of a point in a metric space with respect to an inner product onto a nonempty affine subspace lies in the orthogonal affine subspace of that subspace.
|
EuclideanGeometry.orthogonalProjectionFn_vsub_mem_direction_orthogonal
theorem EuclideanGeometry.orthogonalProjectionFn_vsub_mem_direction_orthogonal :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
EuclideanGeometry.orthogonalProjectionFn s p -ᵥ p ∈ s.direction.orthogonal
This theorem, from the Euclidean Geometry theory in Lean, states that for any point `p` and any affine subspace `s`, the vector obtained by subtracting `p` from its orthogonal projection onto `s` is in the direction orthogonal to `s`. It's important to note that this theorem is meant to be used in the setting up of a more general construct, rather than being used directly in most cases. The types `V` and `P` represent respectively a normed add commutative group and a metric space, while `s.direction.orthogonal` represents the orthogonal direction to the affine subspace `s`.
More concisely: The orthogonal projection of a point onto an affine subspace in a normed add commutative group results in a point whose difference with the original point lies in the direction orthogonal to the subspace.
|
EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal
theorem EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p) ∈ s.direction.orthogonal
This theorem states that for any point `p` and affine subspace `s` equipped with an orthogonal projection in a real inner product space, the vector obtained by subtracting the orthogonal projection of `p` onto `s` from `p` itself lies in the orthogonal complement of the direction of `s`. This is a result from Euclidean geometry, and it essentially says that the difference between a point and its shadow (the projection) on a subspace falls along the direction perpendicular to the subspace.
More concisely: For any point `p` and affine subspace `s` with an orthogonal projection in a real inner product space, the difference between `p` and its orthogonal projection onto `s` lies in the orthogonal complement of the direction of `s`.
|
EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff
theorem EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p : P},
dist p ↑((EuclideanGeometry.orthogonalProjection s) p) = 0 ↔ p ∈ s
This theorem states that for any given point `p` and a subspace `s` in a real inner product space, the distance from `p` to its orthogonal projection onto `s` is zero if and only if the point `p` lies within the subspace `s`. This theorem is a fundamental result in Euclidean Geometry related to orthogonal projections.
More concisely: The theorem asserts that the distance between a point and its orthogonal projection onto a subspace is zero if and only if the point belongs to the subspace.
|
EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq
theorem EuclideanGeometry.reflection_eq_iff_orthogonalProjection_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] (s₁ s₂ : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s₁]
[inst_5 : Nonempty ↥s₂] [inst_6 : HasOrthogonalProjection s₁.direction]
[inst_7 : HasOrthogonalProjection s₂.direction] (p : P),
(EuclideanGeometry.reflection s₁) p = (EuclideanGeometry.reflection s₂) p ↔
↑((EuclideanGeometry.orthogonalProjection s₁) p) = ↑((EuclideanGeometry.orthogonalProjection s₂) p)
The theorem states that for any point in a metric space, reflecting that point in two different subspaces will yield the same result if and only if the point has the same orthogonal projection onto each of those subspaces. The subspaces and the point are in an inner product space over the real numbers, and the subspaces are equipped with an orthogonal projection.
More concisely: In an inner product space over the real numbers, a point has the same reflection in two subspaces equipped with orthogonal projections if and only if it has the same orthogonal projection onto each subspace.
|
EuclideanGeometry.orthogonalProjection_linear
theorem EuclideanGeometry.orthogonalProjection_linear :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction],
(EuclideanGeometry.orthogonalProjection s).linear = ↑(orthogonalProjection s.direction)
The theorem `EuclideanGeometry.orthogonalProjection_linear` states that, for any real inner product space `V`, any metric space `P`, any normed add-torsor `V P`, and any affine subspace `s` of `P` that has an orthogonal projection and is nonempty, the linear map corresponding to the orthogonal projection of `s` is equivalent to the orthogonal projection onto the direction of `s`. In simpler terms, this theorem connects the orthogonal projection in Euclidean geometry with the orthogonal projection onto a subspace in linear algebra, asserting that their associated linear maps are the same.
More concisely: The orthogonal projection of an affine subspace in a Euclidean inner product space onto its orthogonal complement is equivalent to the orthogonal projection onto the subspace's direction.
|
EuclideanGeometry.orthogonalProjection_mem
theorem EuclideanGeometry.orthogonalProjection_mem :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P), ↑((EuclideanGeometry.orthogonalProjection s) p) ∈ s
This theorem states that for any given point 'p' and any subspace 's', the orthogonal projection of the point 'p' onto the subspace 's' lies within the subspace 's'. This is true in the context of Euclidean Geometry and is applicable to any Real Inner Product Space, Metric Space, and Normed Additive Group.
More concisely: In any Real Inner Product Space, Metric Space, or Normed Additive Group, the orthogonal projection of a point onto a subspace lies within that subspace.
|
EuclideanGeometry.reflection_mem_of_le_of_mem
theorem EuclideanGeometry.reflection_mem_of_le_of_mem :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s₁ s₂ : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s₁]
[inst_5 : HasOrthogonalProjection s₁.direction],
s₁ ≤ s₂ → ∀ {p : P}, p ∈ s₂ → (EuclideanGeometry.reflection s₁) p ∈ s₂
This theorem states that, given two subspaces `s₁` and `s₂` of a Euclidean Space with `s₁` contained in `s₂`, and a point `p` in `s₂`, the reflection of point `p` in subspace `s₁` is also contained in `s₂`. The spaces are inner product spaces over real numbers, equipped with a metric and a normed additive group structure. The subspaces are affine subspaces, and it is assumed that `s₁` has a non-empty intersection with the space and has an orthogonal projection.
More concisely: Given a Euclidean Space with inner product, a point in a subspace, and another subspace containing the point and intersecting it nontrivially, the reflection of the point in the smaller subspace lies in the larger subspace.
|
EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection
theorem EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p₁ : P} (p₂ : P) (r : ℝ),
p₁ ∈ s →
(EuclideanGeometry.reflection s) (r • (p₂ -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p₂)) +ᵥ p₁) =
-(r • (p₂ -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p₂))) +ᵥ p₁
This theorem, `EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection`, states that for any given point `p₁` in a subspace `s`, another point `p₂`, and a scalar `r`, the reflection of the vector `r` times the difference between `p₂` and its orthogonal projection onto `s`, when added to `p₁`, is equal to the negation of that same vector added to `p₁`. This is under the conditions that our space is a normed additive commutative group, an inner product space, and a metric space; and `s` is nonempty and has an orthogonal projection.
More concisely: For any point `p₁` in a subspace `s` of a normed additive commutative group and inner product space that is also a metric space, and for any point `p₂` and scalar `r`, the reflection of `r * (p₂ - p₁⊥s)` is equal to `-r * (p₂ - p₁⊥s)` where `p₁⊥s` is the orthogonal projection of `p₁` onto `s`.
|
EuclideanGeometry.dist_reflection_eq_of_mem
theorem EuclideanGeometry.dist_reflection_eq_of_mem :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p₁ : P},
p₁ ∈ s → ∀ (p₂ : P), dist p₁ ((EuclideanGeometry.reflection s) p₂) = dist p₁ p₂
This theorem states that for a given affine subspace `s` in a Euclidean geometry context (where `s` is equipped with a metric, an inner product, and is a normed add torsor), for any point `p₁` that belongs to `s` and any other point `p₂`, the distance from `p₁` to the reflection of `p₂` in `s` is equal to the distance from `p₁` to `p₂`. This means a point and its reflection across the subspace are equidistant from any point on the subspace.
More concisely: For any affine subspace in Euclidean geometry equipped with a metric and inner product, the distance from a point in the subspace to the reflection of another point in the subspace is equal to the distance between the two points.
|
EuclideanGeometry.dist_smul_vadd_sq
theorem EuclideanGeometry.dist_smul_vadd_sq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (r : ℝ) (v : V) (p₁ p₂ : P),
dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ =
⟪v, v⟫_ℝ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ
This theorem states that the squared distance between a point on a line (represented as a scalar multiple of a given vector added to a particular point) and another point is expressed as a quadratic function. The quadratic function is defined in terms of the inner product of the vector with itself (multiplied by the square of the scalar), plus twice the inner product of the vector and the difference between the two points (multiplied by the scalar), plus the inner product of the difference between the two points with itself. Here, the environment must satisfy certain conditions: the vector space has to be a normed add commutative group and an inner product space over the real numbers, and the point space has to be a metric space and a normed add torsor over the vector space.
More concisely: Given a normed add commutative group and inner product space V over the real numbers, and a metric space and normed add torsor X over V, the square distance between two points P and Q on the line L through P with direction vector v is given by the quadratic function ((||v||^2 * ||P - Q||^2) + 2 * (v.inner_product (P - Q))).
|
EuclideanGeometry.reflection_eq_self_iff
theorem EuclideanGeometry.reflection_eq_self_iff :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P), (EuclideanGeometry.reflection s) p = p ↔ p ∈ s
This theorem states that for any point `p` in a Euclidean space with a given affine subspace `s`, the reflection of `p` with respect to `s` is equal to `p` itself if and only if `p` belongs to the subspace `s`. This is true for any normed add commutative group `V` and any inner product space over the real numbers `ℝ`, where `P` is a metric space that forms a normed add torsor over `V`, and `s` has a defined orthogonal projection.
More concisely: The reflection of a point `p` in a Euclidean space with respect to a subspace `s` is equal to `p` if and only if `p` belongs to `s`.
|
EuclideanGeometry.orthogonalProjection_vadd_eq_self
theorem EuclideanGeometry.orthogonalProjection_vadd_eq_self :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p : P} (hp : p ∈ s) {v : V},
v ∈ s.direction.orthogonal → (EuclideanGeometry.orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩
The theorem `EuclideanGeometry.orthogonalProjection_vadd_eq_self` states that for any given subspace `s` in a Euclidean geometry with associated vector space `V` and point space `P`, and for any point `p` in `s` and vector `v` orthogonal to `s`, if we add the vector `v` to the point `p` and then take the orthogonal projection of the resulting point onto `s`, we will get back the original point `p`. This is essentially saying that if we move away from a point in a direction orthogonal to a subspace, and then project back onto that subspace, we revert to our original position. The theorem requires the usual structures for dealing with Euclidean geometry, inner products, normed add-commutative groups, and metric spaces, as well as the existence of an orthogonal projection for the direction of `s`.
More concisely: For any point `p` in a subspace `s` of a Euclidean geometry with associated vector space `V`, and any vector `v` orthogonal to `s`, the orthogonal projection of `p + v` onto `s` equals `p`.
|
EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
theorem EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
↑((EuclideanGeometry.orthogonalProjection s) p) -ᵥ p ∈ s.direction.orthogonal
This theorem states that in a Euclidean geometry, when you subtract a point `p` from its orthogonal projection onto an affine subspace `s`, the result lies in the orthogonal direction to the subspace `s`. The prerequisites for this theorem include: `V` is a normed additive commutative group, `V` has an inner product space over real numbers, `P` is a metric space, `P` is a normed additive torsor over `V`, `s` is a nonempty affine subspace of `P`, and `s` has an orthogonal projection.
More concisely: In a Euclidean geometry, the difference between a point and its orthogonal projection onto an affine subspace lies in the orthogonal direction to the subspace.
|
EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection
theorem EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
(orthogonalProjection s.direction) (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)) = 0
The theorem `EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection` states that for any point `p` and a given affine subspace `s` in a real inner product space, if we subtract the orthogonal projection of `p` onto `s` from `p`, and then find the orthogonal projection of this result onto the direction of `s`, the final result will be zero. This theorem essentially asserts that the result of the subtraction operation mentioned lies in the kernel of the linear part of the orthogonal projection onto the direction of `s`.
More concisely: The orthogonal projection of the difference between a point and its orthogonal projection onto an affine subspace onto the direction of the subspace is zero.
|
EuclideanGeometry.orthogonalProjection_orthogonalProjection
theorem EuclideanGeometry.orthogonalProjection_orthogonalProjection :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
(EuclideanGeometry.orthogonalProjection s) ↑((EuclideanGeometry.orthogonalProjection s) p) =
(EuclideanGeometry.orthogonalProjection s) p
This theorem states that the orthogonal projection operation in Euclidean geometry is idempotent. Given a subspace `s` of a normed additive torsor over an inner product space `V` and a point `p`, the orthogonal projection of `p` onto `s` remains the same even after applying the orthogonal projection operation again. In mathematical terms, if `Proj` denotes the orthogonal projection, then for any point `p` in the space, `Proj(Proj(p))` is equal to `Proj(p)`. This property of idempotence is crucial for many geometric computations and simplifications.
More concisely: The orthogonal projection of a point onto a subspace in an inner product space is idempotent, i.e., applying the projection operation twice results in the same output as applying it once.
|
EuclideanGeometry.dist_reflection
theorem EuclideanGeometry.dist_reflection :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p₁ p₂ : P),
dist p₁ ((EuclideanGeometry.reflection s) p₂) = dist ((EuclideanGeometry.reflection s) p₁) p₂
The theorem `EuclideanGeometry.dist_reflection` states that for any two points `p₁` and `p₂` in a Euclidean space, the distance from `p₁` to the reflection of `p₂` across an affine subspace `s` is equal to the distance from the reflection of `p₁` across `s` to `p₂`. This theorem holds for any normed additive commutative group `V` with an inner product space over the real numbers, any metric space `P`, and any normed additive torsor `V` acting on `P`.
More concisely: Given points `p₁` and `p₂` in a Euclidean space, the distance between `p₁` and the reflection of `p₂` across an affine subspace `s` equals the distance between the reflection of `p₁` across `s` and `p₂`.
|
EuclideanGeometry.reflection_apply
theorem EuclideanGeometry.reflection_apply :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
(EuclideanGeometry.reflection s) p =
↑((EuclideanGeometry.orthogonalProjection s) p) -ᵥ p +ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)
This theorem states that for any vector space `V` with an associated point space `P`, given a subspace `s` of `P` and a point `p` in `P`, the reflection of `p` over `s` is equal to twice the orthogonal projection of `p` onto `s` minus `p`. This is under the assumptions that `V` forms a normed add commutative group, `V` has an inner-product structure with real numbers, `P` is a metric space, `V` is a normed add torsor for `P`, `s` is not empty, and the direction of `s` has an orthogonal projection.
More concisely: For any vector space `V` with a metric space point space `P`, given a subspace `s` of `P`, and a point `p` in `P` such that `s` is non-empty and has an orthogonal projection, the reflection of `p` over `s` equals twice the orthogonal projection of `p` onto `s` minus `p`.
|
EuclideanGeometry.dist_left_midpoint_eq_dist_right_midpoint
theorem EuclideanGeometry.dist_left_midpoint_eq_dist_right_midpoint :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (p1 p2 : P),
dist p1 (midpoint ℝ p1 p2) = dist p2 (midpoint ℝ p1 p2)
This theorem states that for any two points, known as `p1` and `p2`, in a Euclidean space, the Euclidean distance from `p1` to the midpoint of the line segment between `p1` and `p2` is equal to the Euclidean distance from `p2` to the same midpoint. In other words, the midpoint is equidistant from the two endpoints of the line segment.
More concisely: In a Euclidean space, the midpoint of the line segment between two points equals the average of those points, and the Euclidean distance from each point to the midpoint is equal.
|
EuclideanGeometry.inner_weightedVSub
theorem EuclideanGeometry.inner_weightedVSub :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {ι₁ : Type u_3} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ}
(p₁ : ι₁ → P),
(s₁.sum fun i => w₁ i) = 0 →
∀ {ι₂ : Type u_4} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P),
(s₂.sum fun i => w₂ i) = 0 →
⟪(s₁.weightedVSub p₁) w₁, (s₂.weightedVSub p₂) w₂⟫_ℝ =
(-s₁.sum fun i₁ => s₂.sum fun i₂ => w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
The theorem `EuclideanGeometry.inner_weightedVSub` states that for any two sets of vectors (described by the types `ι₁` and `ι₂`), represented with the function `weightedVSub`, in a Euclidean space with an inner product and a metric, if the sum of weights for each set of vectors is zero, then the inner product of these two sets of vectors is equal to negative one half of the sum of the product of the weights and the square of the distance between each pair of points, summed over all pairs of points from the two sets.
More concisely: For sets of vectors in a Euclidean space with an inner product and metric, if their weighted differences have zero total weight, then their inner product is equal to negative half the sum of the weights' products with the squared distances between corresponding vectors.
|
EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection
theorem EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p1 : P} (p2 : P) (r : ℝ) (hp : p1 ∈ s),
(EuclideanGeometry.orthogonalProjection s) (r • (p2 -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p2)) +ᵥ p1) =
⟨p1, hp⟩
This theorem, in the context of Euclidean Geometry, states that for any given subspace `s`, and any points `p1` and `p2` and real number `r`, if `p1` belongs to `s`, adding `r` times the vector from the orthogonal projection of `p2` on `s` to `p2` to `p1`, and then taking the orthogonal projection on `s`, yields `p1`. Essentially, it says that the orthogonal projection of a point `p1` in the subspace, displaced by a vector that is a multiple of the difference between `p2` and its orthogonal projection, remains `p1`. This theorem is a key property of orthogonal projection in the mathematical field of vector spaces and affine geometry.
More concisely: Given a subspace `s`, point `p1` in `s`, and point `p2` with orthogonal projection `p` on `s`, the point `p1 + r(p2 - p)` is the orthogonal projection of `p1 + r(p2 - p)` onto `s`, where `r` is any real number.
|
EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_finrank_eq_two
theorem EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_finrank_eq_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [inst_4 : FiniteDimensional ℝ V],
FiniteDimensional.finrank ℝ V = 2 →
∀ {c₁ c₂ p₁ p₂ p : P} {r₁ r₂ : ℝ},
c₁ ≠ c₂ →
p₁ ≠ p₂ →
dist p₁ c₁ = r₁ →
dist p₂ c₁ = r₁ →
dist p c₁ = r₁ → dist p₁ c₂ = r₂ → dist p₂ c₂ = r₂ → dist p c₂ = r₂ → p = p₁ ∨ p = p₂
This theorem states that if we have a two-dimensional vector space over the real numbers (i.e., its rank as a module over the reals is 2), and we have five points (`c₁`, `c₂`, `p₁`, `p₂`, `p`) and two distances `r₁` and `r₂`. If `c₁` and `c₂` are different points, and `p₁` and `p₂` are also different points, and if the distances from `p₁`, `p₂`, and `p` to `c₁` are all `r₁`, and the distances from `p₁`, `p₂`, and `p` to `c₂` are all `r₂`, then `p` must either coincide with `p₁` or `p₂`. In plain terms, the theorem relates to Euclidean geometry and states that two circles in the plane intersect in at most two points.
More concisely: Given a two-dimensional real vector space and distinct points `c₁`, `c₂`, `p₁`, `p₂`, and `p` with equal distances `r₁` to `c₁` and `r₂` to `c₂`, if the distances of `p₁`, `p₂`, and `p` to `c₁` and `c₂` are equal to `r₁` and `r₂`, respectively, then `p` lies on the line connecting `p₁` and `p₂`.
|
EuclideanGeometry.reflection_symm
theorem EuclideanGeometry.reflection_symm :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction],
(EuclideanGeometry.reflection s).symm = EuclideanGeometry.reflection s
This theorem states that reflection in Euclidean geometry is its own inverse. This is applicable for any affine subspace, given that the space belongs to a metric space, is a normed add torsor for a vector space that is a normed add commutative group and has an inner product space over the real numbers. Additionally, the direction of the subspace must have an orthogonal projection and the subspace must be nonempty. In other words, the reflection of a point through a subspace is the same when reflected back through the same subspace.
More concisely: The reflection of a point through an orthogonal, nonempty, and normed affine subspace of a real inner product space is its own inverse.
|
EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq
theorem EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p1 : P} (p2 : P),
p1 ∈ s →
dist p1 p2 * dist p1 p2 =
dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p2) *
dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p2) +
dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p2) *
dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p2)
This theorem states that in a real inner product space, for any given point `p1` in an affine subspace `s` and another point `p2`, the square of the distance between `p1` and `p2` is equal to the sum of squares of their distances to the orthogonal projection of `p2` onto `s`. This is essentially a statement of the Pythagorean theorem in the context of inner product spaces and affine subspaces.
More concisely: In a real inner product space, the square of the distance between two points in an affine subspace is equal to the sum of the squares of their distances to the subspace's orthogonal projection.
|
EuclideanGeometry.dist_affineCombination
theorem EuclideanGeometry.dist_affineCombination :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {ι : Type u_3} {s : Finset ι} {w₁ w₂ : ι → ℝ} (p : ι → P),
(s.sum fun i => w₁ i) = 1 →
(s.sum fun i => w₂ i) = 1 →
let_fun a₁ := (Finset.affineCombination ℝ s p) w₁;
let_fun a₂ := (Finset.affineCombination ℝ s p) w₂;
dist a₁ a₂ * dist a₁ a₂ =
(-s.sum fun i₁ => s.sum fun i₂ => (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) /
2
This theorem states that in a Euclidean space with an associated inner product space and metric space, the squared distance between two points, each obtained by an affine combination of a set of points, can be expressed in terms of the pairwise distances between the points used in that combination. Specifically, the squared distance between the two points is negative half of the sum, over all pairs of points in the set, of the product of the differences in the weights of the two points in the affine combinations and the squared distance between the two points. This is under the precondition that the weights used in the two affine combinations each sum up to 1.
More concisely: In a Euclidean space with an inner product, the squared distance between two affine combinations of points, whose weights sum to 1 for each point set, is equal to negative half the sum of the weighted squared pairwise distances between the points in the sets.
|
EuclideanGeometry.dist_smul_vadd_eq_dist
theorem EuclideanGeometry.dist_smul_vadd_eq_dist :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {v : V} (p₁ p₂ : P),
v ≠ 0 → ∀ (r : ℝ), dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ / ⟪v, v⟫_ℝ
This theorem states the condition for two points on a line to be equidistant from another point in the context of Euclidean geometry. Specifically, for a given normed add commutative group `V`, inner product space over the reals `ℝ`, metric space `P`, and a normed add torsor over `V` and `P`, if `v ≠ 0`, then the distance between `r * v + p₁` and `p₂` is equal to the distance between `p₁` and `p₂` if and only if `r` equals `0` or `r` equals `-2 * inner_product(v, p₁ - p₂) / inner_product(v, v)`.
More concisely: For a given normed add commutative group `V`, inner product space over the reals `ℝ`, metric space `P`, and a normed add torsor over `V` and `P`, the distance between `r * v + p₁` and `p₂` equals the distance between `p₁` and `p₂` if and only if `r` is equal to `0` or `-2 * / `, where `<.,.>` denotes the inner product.
|
EuclideanGeometry.orthogonalProjection_vsub_mem_direction
theorem EuclideanGeometry.orthogonalProjection_vsub_mem_direction :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p1 : P} (p2 : P) (hp1 : p1 ∈ s),
↑((EuclideanGeometry.orthogonalProjection s) p2 -ᵥ ⟨p1, hp1⟩) ∈ s.direction
The theorem `EuclideanGeometry.orthogonalProjection_vsub_mem_direction` states that for any points `p1` and `p2` and a given subspace `s`, if `p1` is in the subspace `s`, then the vector obtained by subtracting `p1` from the orthogonal projection of `p2` onto the subspace `s` is a direction vector of the subspace `s`. Here, the orthogonal projection refers to the nearest point in the subspace `s` from the point `p2`. This theorem is a part of Euclidean geometry and relies on the properties of inner product spaces and normed add torsors.
More concisely: If point `p1` is in subspace `s`, then the vector `p2 - proj_s p2` is a direction vector of `s`, where `proj_s p2` is the orthogonal projection of `p2` onto `s`.
|
EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd
theorem EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {p1 p2 : P},
p1 ∈ s →
p2 ∈ s →
∀ (r1 r2 : ℝ) {v : V},
v ∈ s.direction.orthogonal →
dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) =
dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (‖v‖ * ‖v‖)
This theorem is about the Euclidean geometry in a metric space. It states that given a normed add torsor and an inner product space over the reals, along with an affine subspace 's' and two points p1 and p2 in 's', for any two real numbers r1 and r2 and a vector 'v' which is orthogonal to the direction of 's', the square of the distance between two points which are constructed by adding multiples (r1 and r2) of the same orthogonal vector 'v' to the points p1 and p2, is equal to the sum of the square of the distance between p1 and p2 and the product of the square of the difference between r1 and r2 and the squared norm of 'v'.
More concisely: Given a normed additive torsor and an inner product space over the reals, for any affine subspace, points p1 and p2 in it, real numbers r1 and r2, and orthogonal vector v, the square of the distance between the points p1 + rv and p2 + r2v is equal to the sum of the square of the distance between p1 and p2 and the product of the squared norm of v and the square of the difference between r1 and r2.
|
EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two
theorem EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P}
[inst_4 : FiniteDimensional ℝ ↥s.direction],
FiniteDimensional.finrank ℝ ↥s.direction = 2 →
∀ {c₁ c₂ p₁ p₂ p : P},
c₁ ∈ s →
c₂ ∈ s →
p₁ ∈ s →
p₂ ∈ s →
p ∈ s →
∀ {r₁ r₂ : ℝ},
c₁ ≠ c₂ →
p₁ ≠ p₂ →
dist p₁ c₁ = r₁ →
dist p₂ c₁ = r₁ →
dist p c₁ = r₁ → dist p₁ c₂ = r₂ → dist p₂ c₂ = r₂ → dist p c₂ = r₂ → p = p₁ ∨ p = p₂
The theorem named `EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two` states that in a two-dimensional subspace, if we have two distinct points `c₁` and `c₂`, and we consider three points `p₁`, `p₂`, and `p` such that the distances from `p₁`, `p₂`, and `p` to `c₁` are all `r₁` and the distances from `p₁`, `p₂`, and `p` to `c₂` are all `r₂`, then point `p` is either `p₁` or `p₂`. This is analogous to the geometrical assertion that two circles, defined by the distances `r₁` and `r₂` from `c₁` and `c₂` respectively, intersect at at most two points.
More concisely: In a two-dimensional subspace, if three points have the same distances to two distinct points, then the three points are collinear and lie on a segment connecting the two distinct points.
|
EuclideanGeometry.orthogonalProjectionFn_mem_orthogonal
theorem EuclideanGeometry.orthogonalProjectionFn_mem_orthogonal :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] (p : P),
EuclideanGeometry.orthogonalProjectionFn s p ∈ AffineSubspace.mk' p s.direction.orthogonal
This theorem states that in a Euclidean geometry setup, the orthogonal projection of a point onto an affine subspace lies in the orthogonal affine subspace to the direction of the original subspace. This result is specific to the context where the underlying vector space is endowed with an inner product and the point space is a metric space. However, this theorem is intended primarily for setting up the bundled version of orthogonal projections and is not recommended for use once that version is established.
More concisely: In Euclidean geometry with an inner product, the orthogonal projection of a point onto an affine subspace lies in the subspace orthogonal to the direction of the original subspace.
|
EuclideanGeometry.reflection_orthogonal_vadd
theorem EuclideanGeometry.reflection_orthogonal_vadd :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
[inst_5 : HasOrthogonalProjection s.direction] {p : P},
p ∈ s → ∀ {v : V}, v ∈ s.direction.orthogonal → (EuclideanGeometry.reflection s) (v +ᵥ p) = -v +ᵥ p
This theorem states that in a real inner product space, given a subspace `s` and a point `p` in the subspace, for any vector `v` that is orthogonal to the direction of the subspace, the reflection of the vector `v` added to the point `p` with respect to subspace `s` is equal to the negation of the vector `v` added to the point `p`.
In other words, reflecting a vector orthogonal to a subspace, together with a point in the subspace, produces the negative of the vector plus the point.
More concisely: In a real inner product space, for any subspace `s`, point `p` in `s`, and orthogonal vector `v`, the reflection of `v` about `s` at `p` equals `p - v`.
|