EuclideanGeometry.Sphere.secondInter_mem
theorem EuclideanGeometry.Sphere.secondInter_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 : EuclideanGeometry.Sphere P} {p : P} (v : V),
s.secondInter p v ∈ s ↔ p ∈ s
This theorem states that for any point `p` and vector `v` in a Euclidean space, the point obtained by the `secondInter` operation lies on a given sphere `s` if and only if `p` itself lies on the sphere `s`. The space is defined over a normed additive commutative group `V` and inner product space with real numbers, and `P` is a metric space with a normed additive torsor structure over `V`. The `secondInter` operation refers to finding a second point of intersection between a vector and the sphere.
More concisely: For any point `p` and vector `v` in a Euclidean space over a normed additive commutative group `V` and inner product space with real numbers, and for a sphere `s` in the metric space `P` over `V`, the point obtained by finding the second intersection of `p` and `v` with `s` lies on `s` if and only if `p` itself lies on `s`.
|
EuclideanGeometry.Sphere.secondInter_neg
theorem EuclideanGeometry.Sphere.secondInter_neg :
∀ {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 : EuclideanGeometry.Sphere P) (p : P) (v : V),
s.secondInter p (-v) = s.secondInter p v
The theorem `EuclideanGeometry.Sphere.secondInter_neg` states that for any sphere in a Euclidean space, any point on the space, and any vector, the second intersection of the sphere with a line from the point in the direction of the negated vector is the same as the second intersection of the sphere with a line from the point in the direction of the original vector. Essentially, it says that negating the direction of the vector does not change the second intersection point of the sphere.
More concisely: For any sphere in a Euclidean space, the second intersection point of the sphere with a line through the sphere's center in the direction of a vector is equal to the second intersection point with the line in the direction of the vector's negation.
|
EuclideanGeometry.Sphere.secondInter_secondInter
theorem EuclideanGeometry.Sphere.secondInter_secondInter :
∀ {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 : EuclideanGeometry.Sphere P) (p : P) (v : V),
s.secondInter (s.secondInter p v) v = p
This theorem states that for any point `p` and vector `v`, applying the `secondInter` function of a Euclidean sphere `s` twice on `p` with respect to `v` yields the original point `p` itself. In other words, it's like the second intersection is an operation which undoes itself when applied twice. Here, `secondInter` is presumably a function in the context of Euclidean geometry that gives the second intersection of a line (defined by a point and a vector) with a sphere.
More concisely: For any point `p` and vector `v` in Euclidean space, applying the `secondInter` function of a Euclidean sphere `s` twice with respect to `p` and `v` returns `p`.
|
EuclideanGeometry.Sphere.secondInter_eq_self_iff
theorem EuclideanGeometry.Sphere.secondInter_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 : EuclideanGeometry.Sphere P} {p : P} {v : V},
s.secondInter p v = p ↔ ⟪v, p -ᵥ s.center⟫_ℝ = 0
This theorem states that for a given point `p` and a vector `v` in a Euclidean Space, the secondary intersection of the vector with a sphere `s` equals the original point `p` if and only if the inner product of the vector `v` and the displacement vector from the center of the sphere to the point `p` is zero. In other words, the line represented by the vector `v` is orthogonal (perpendicular) to the radius vector of the sphere.
More concisely: A vector is orthogonal to the radius vector of a sphere at a point if and only if the point lies on the secondary intersection of the vector and the sphere.
|
EuclideanGeometry.Sphere.secondInter_smul
theorem EuclideanGeometry.Sphere.secondInter_smul :
∀ {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 : EuclideanGeometry.Sphere P) (p : P) (v : V) {r : ℝ},
r ≠ 0 → s.secondInter p (r • v) = s.secondInter p v
The theorem `EuclideanGeometry.Sphere.secondInter_smul` states that for any Euclidean sphere 's', point 'p', vector 'v', and nonzero real number 'r', the second intersection of the sphere 's' with the line passing through 'p' in the direction of 'r' times the vector 'v' (r • v) is the same as the second intersection of the sphere 's' with the line passing through 'p' in the direction of the vector 'v'. In other words, scaling the direction vector by a nonzero real number doesn't change the second intersection point of the line with the sphere.
More concisely: For any Euclidean sphere 's', point 'p', vector 'v' and nonzero real number 'r', the second intersection of sphere 's' with the line through 'p' in direction 'r' • 'v' equals the second intersection with the line through 'p' in direction 'v'.
|
EuclideanGeometry.Sphere.wbtw_secondInter
theorem EuclideanGeometry.Sphere.wbtw_secondInter :
∀ {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 : EuclideanGeometry.Sphere P} {p p' : P},
p ∈ s → dist p' s.center ≤ s.radius → Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
In the context of Euclidean geometry, this theorem states that given a Euclidean sphere `s`, and any two points `p` and `p'` such that `p` is on the sphere and `p'` is not outside the sphere, the function `secondInter` is defined in such a way that `p'` is weakly between `p` and the result of `secondInter` when the vector passed to `secondInter` is the result of subtracting `p` from `p'`. Here, being weakly between means that `p'` lies on the straight line segment connecting `p` and the result of `secondInter`.
More concisely: In Euclidean geometry, given a sphere and two points on it with one point inside and the other not outside, the second point lies on the straight line segment connecting the first point and the point of intersection of the line passing through the first and second points and the sphere.
|
EuclideanGeometry.Sphere.secondInter_zero
theorem EuclideanGeometry.Sphere.secondInter_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] (s : EuclideanGeometry.Sphere P) (p : P),
s.secondInter p 0 = p
This theorem states that in Euclidean geometry, given any sphere `s` and point `p`, if the vector is zero, the `secondInter` function will produce the original point `p`. Here, the types `V` and `P` denote the vector and point spaces respectively, with `V` being a normed additive commutative group, a real inner product space, and `P` being a metric space and a normed additive torsor over `V`.
More concisely: In Euclidean geometry, for any sphere `s` and point `p`, if the vector `p - center s` is the zero vector, then `secondInter s p` equals point `p`.
|
EuclideanGeometry.Sphere.secondInter_collinear
theorem EuclideanGeometry.Sphere.secondInter_collinear :
∀ {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 : EuclideanGeometry.Sphere P) (p p' : P),
Collinear ℝ {p, p', s.secondInter p (p' -ᵥ p)}
The theorem "EuclideanGeometry.Sphere.secondInter_collinear" states that for any given sphere in Euclidean geometry and any two points `p` and `p'`, if the vector passed to the `secondInter` function is obtained by subtracting the location vector of the point `p` from that of `p'`, then these three points - `p`, `p'`, and the second intersection of the sphere with the line determined by `p` and `p'` - are collinear. In other words, these three points lie on the same straight line.
More concisely: Given a sphere in Euclidean geometry and points `p` and `p'` on it, the second intersection point `q` of the sphere with the line passing through `p` and `p'`, the points `p`, `p'`, and `q` are collinear.
|
EuclideanGeometry.Sphere.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem
theorem EuclideanGeometry.Sphere.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_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 : EuclideanGeometry.Sphere P} {p : P},
p ∈ s →
∀ {v : V} {p' : P},
p' ∈ AffineSubspace.mk' p (Submodule.span ℝ {v}) → (p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s)
The theorem `EuclideanGeometry.Sphere.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem` states that for a given Euclidean sphere `s` and a point `p` on the sphere, and for any vector `v` and point `p'` in the affine subspace formed by `p` and the span of `v`, the point `p'` is either equal to `p` or it is the second intersection of the line going through `p` along vector `v` with the sphere `s` if and only if `p'` is a point on the sphere `s`.
More concisely: Given a Euclidean sphere and a point on it, a vector and another point in the line passing through the first point in the direction of the vector, the second intersection point of the line with the sphere is either equal to the first point or it is the unique point on the line intersecting the sphere if and only if the second point lies on the sphere.
|
EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan
theorem EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan :
∀ {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 : EuclideanGeometry.Sphere P) (p₁ p₂ : P),
s.secondInter p₁ (p₂ -ᵥ p₁) ∈ affineSpan ℝ {p₁, p₂}
The theorem `EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan` states that for any sphere `s` and any two points `p₁` and `p₂` in a Euclidean geometry, when a vector, given by the subtraction of `p₁` from `p₂`, is passed to the `secondInter` function of the sphere, the resulting point lies in the affine span of the two points `p₁` and `p₂`. An affine span is the smallest affine subspace containing the given points. This theorem is set within the context of normed addition commutative groups, inner product spaces, metric spaces, and normed addition torsors.
More concisely: Given a sphere in Euclidean geometry and any two of its points, the point lying on the sphere that is the second intersection of the sphere with the line passing through these two points is in the affine span of these two points.
|
EuclideanGeometry.Sphere.secondInter_eq_lineMap
theorem EuclideanGeometry.Sphere.secondInter_eq_lineMap :
∀ {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 : EuclideanGeometry.Sphere P) (p p' : P),
s.secondInter p (p' -ᵥ p) = (AffineMap.lineMap p p') (-2 * ⟪p' -ᵥ p, p -ᵥ s.center⟫_ℝ / ⟪p' -ᵥ p, p' -ᵥ p⟫_ℝ)
The theorem `EuclideanGeometry.Sphere.secondInter_eq_lineMap` states that for any normed add commutative group `V`, any type `P` with a metric space structure and an instance of normed add torsor over `V`, any Euclidean sphere `s` in `P`, and any two points `p` and `p'` in `P`, if the vector passed to the `secondInter` function is a result of the subtraction of `p` from `p'`, then the result of the `secondInter` function can be described using the `AffineMap.lineMap` function. Specifically, it can be expressed as the application of `AffineMap.lineMap` with arguments `p` and `p'` to the quantity `-2 * ⟪p' -ᵥ p, p -ᵥ s.center⟫_ℝ / ⟪p' -ᵥ p, p' -ᵥ p⟫_ℝ`. This quantity corresponds to the dot product between the vectors `p' -ᵥ p` and `p -ᵥ s.center`, multiplied by -2 and divided by the dot product of the vector `p' -ᵥ p` with itself.
More concisely: Given a normed add commutative group `V`, a metric space `P` with a normed add torsor structure over `V`, an Euclidean sphere `s` in `P`, and points `p` and `p'` in `P`, if the vector `p' - p` is the argument to the `secondInter` function, then the result is equal to the application of `AffineMap.lineMap` with arguments `p` and `p'` to the scalar `-2 * (p' - p) · (p - s.center) / ||p' - p||²`.
|
EuclideanGeometry.Sphere.sbtw_secondInter
theorem EuclideanGeometry.Sphere.sbtw_secondInter :
∀ {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 : EuclideanGeometry.Sphere P} {p p' : P},
p ∈ s → dist p' s.center < s.radius → Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
This theorem states that in a Euclidean geometry, given a sphere and two points `p` and `p'`, if `p` lies on the sphere and `p'` is closer to the center of the sphere than its radius, then the point `p'` lies strictly between the point `p` and a third point. This third point is the second intersection point on the sphere of a line passing through `p'` and `p`, where the vector directing the line is given by the subtraction of the positions of `p` and `p'`.
More concisely: In Euclidean geometry, if a point `p'` lies strictly inside a sphere with center `C` and radius `r`, and `p` is a point on the sphere, then there exists a third point `q` on the line passing through `p` and `p'` such that `C` is between `p` and `q`.
|
EuclideanGeometry.Sphere.secondInter_dist
theorem EuclideanGeometry.Sphere.secondInter_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] (s : EuclideanGeometry.Sphere P) (p : P) (v : V),
dist (s.secondInter p v) s.center = dist p s.center
This theorem, from Euclidean Geometry, states that the distance between a point referred to as `secondInter` and the center of a sphere is equal to the distance between the original point and the center of the sphere. This holds true for any sphere `s`, any original point `p`, and any vector `v`. The sphere, the points, and the vector all exist in a normed add torsor, which is a space that supports vector addition and scalar multiplication. The vector space is also an inner product space, meaning it supports an inner product operation.
More concisely: The distance from a point `secondInter` to the center of a sphere is equal to the distance from another point `p` to the center, for any sphere `s`, point `p`, and vector `v` in a normed additive torsor and inner product space.
|