Affine.Simplex.vectorSpan_isOrtho_altitude_direction
theorem Affine.Simplex.vectorSpan_isOrtho_altitude_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] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1))
(i : Fin (n + 2)), (vectorSpan ℝ (s.points '' ↑(Finset.univ.erase i))).IsOrtho (s.altitude i).direction
This theorem states that for any normed additive commutative group `V`, any inner product space over real numbers with `V`, any metric space `P`, and any normed additive torsor `V` over `P`; given a natural number 'n' and an affine simplex 's' in `P` with dimension 'n+1', for any index 'i' in the finite set from 0 to 'n+2', the vector span of the set of points in the simplex, excluding the point at index 'i', is orthogonal to the direction of the altitude of the simplex at index 'i'. In other words, the direction of an altitude of an affine simplex is orthogonal to the vectors spanning the opposite face.
More concisely: For any affine simplex in a normed additive commutative group, the direction of an altitude is orthogonal to the span of the opposite face's vectors.
|
Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset
theorem Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ : Fin 3},
i₁ ≠ i₂ →
dist t.orthocenter
((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' ↑{i₁, i₂}))) (Affine.Simplex.circumcenter t)) =
Affine.Simplex.circumradius t
The theorem `Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset` states that for any given affine triangle (denoted by `t`), and any two distinct vertices of the triangle (denoted by `i₁` and `i₂`), the Euclidean distance between the orthocenter of the triangle and the reflection of the circumcenter of the triangle in the side spanned by the two distinct vertices equals the circumradius of the triangle. Here, `EuclideanGeometry.reflection` represents reflection in a point or a line, and `affineSpan ℝ (t.points '' ↑{i₁, i₂})` yields the line or affine subspace spanned by the two distinct vertices. The orthocenter of a triangle is the point where the three altitudes of the triangle intersect. The circumcenter of a triangle is the center of the circle that passes through all three vertices of the triangle, and the circumradius is the radius of that circle.
More concisely: The distance between the orthocenter and the reflection of the circumcenter of an affine triangle in the line through two distinct vertices equals the circumradius.
|
Affine.Triangle.eq_orthocenter_of_forall_mem_altitude
theorem Affine.Triangle.eq_orthocenter_of_forall_mem_altitude :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {t : Affine.Triangle ℝ P} {i₁ i₂ : Fin 3} {p : P},
i₁ ≠ i₂ → p ∈ Affine.Simplex.altitude t i₁ → p ∈ Affine.Simplex.altitude t i₂ → p = t.orthocenter
The theorem `Affine.Triangle.eq_orthocenter_of_forall_mem_altitude` states that for any given affine triangle (a collection of three affinely independent points), the orthocenter (the common intersection of the lines of the triangle that are perpendicular to its sides) is the unique point that lies on any two of the triangle's altitudes (the perpendicular lines from a vertex to the line containing the opposite side). More formally, given a triangle and two different indices from the set {0,1,2}, if a point `p` belongs to the altitudes corresponding to these indices, then `p` is the orthocenter of the triangle.
More concisely: The orthocenter of an affine triangle is the unique point that lies on the altitudes corresponding to any two of its vertices.
|
Affine.Simplex.mongePlane_comm
theorem Affine.Simplex.mongePlane_comm :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2))
(i₁ i₂ : Fin (n + 3)), s.mongePlane i₁ i₂ = s.mongePlane i₂ i₁
This theorem states that for any affine simplex `s` with vertices indexed by numbers `i₁` and `i₂`, the Monge plane associated with `i₁` and `i₂` is the same as the Monge plane associated with `i₂` and `i₁`. This statement holds true in a normed add torsor over an inner product space over the real numbers. In simpler terms, changing the order of indices does not change the Monge plane associated with those indices.
More concisely: The Monge plane of two vertices in an affine simplex over an inner product space is commutative, i.e., the Monge plane for vertices `i₁` and `i₂` is equal to the Monge plane for `i₂` and `i₁`.
|
Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter
theorem Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)),
s.mongePoint =
(Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter)
(Affine.Simplex.mongePointWeightsWithCircumcenter n)
The theorem `Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter` states that for any real number (ℝ) affine (n+2)-simplex 's', the Monge point of this simplex is equivalent to the affine combination of the points with circumcenter of the simplex. This affine combination is computed with respect to the entire set of points in the simplex (`Finset.univ s.pointsWithCircumcenter`) and uses the weights defined by `Affine.Simplex.mongePointWeightsWithCircumcenter n`. Here 'n' is a natural number representing the dimension of the simplex, 'V' is the normed additive commutative group representing the vector space, 'P' is the metric space representing the point set, and ℝ represents the field of real numbers. The vector space 'V' is also an inner product space over the real numbers.
More concisely: The Monge point of an n-dimensional real affine simplex is equivalent to the affine combination of its circumcenter and the simplex's points, using the weights defined by `Affine.Simplex.mongePointWeightsWithCircumcenter n`.
|
Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub
theorem Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2))
{i₁ i₂ : Fin (n + 3)}, ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫_ℝ = 0
The theorem `Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub` states that for any (n+2)-simplex defined over real numbers, if we take the Monge point of the simplex, subtract the centroid of an n-dimensional face (a subset of the simplex's vertices), and take the inner product of this difference with the difference of two vertices not in that face, the result will be zero. In other words, the vector from the centroid to the Monge point is orthogonal to the vector between the two vertices not included in the centroid calculation. This is a characteristic of Monge points in affine geometry.
More concisely: For any (n+2)-simplex over real numbers, the vector from the Monge point to the centroid of an n-dimensional face is orthogonal to the edge between two non-coinciding vertices of the simplex not in that face.
|
EuclideanGeometry.OrthocentricSystem.affineIndependent
theorem EuclideanGeometry.OrthocentricSystem.affineIndependent :
∀ {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 : Set P},
EuclideanGeometry.OrthocentricSystem s →
∀ {p : Fin 3 → P}, Set.range p ⊆ s → Function.Injective p → AffineIndependent ℝ p
This theorem states that any three points within an orthocentric system are affinely independent. In the context of Euclidean Geometry, an orthocentric system is defined as a set of four points, which are the vertices of a triangle and its orthocenter. Affine independence here means that no nontrivial weighted subtraction of these points, where the sum of weights is zero, equals zero. Thus, for any set of points forming an orthocentric system, if a function maps from the set of first three natural numbers to this set of points and is injective, then this function's output, the three points, are affinely independent.
More concisely: In the context of Euclidean Geometry, the three points of an orthocentric system are affinely independent.
|
Affine.Simplex.finrank_direction_altitude
theorem Affine.Simplex.finrank_direction_altitude :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1))
(i : Fin (n + 2)), FiniteDimensional.finrank ℝ ↥(s.altitude i).direction = 1
This theorem states that the rank of the direction of an altitude of an affine simplex, which can be thought of as a generalized triangle in an affine space, is one. In other words, the direction of an altitude is one-dimensional, or equivalently, it is a line. This applies to any affine simplex in a normed add commutative group with an inner product space over real numbers, with metric space and normed add torsor structures.
More concisely: The direction of an altitude of an affine simplex in a normed add commutative group with an inner product space over real numbers is a one-dimensional subspace.
|
Affine.Simplex.affineSpan_pair_eq_altitude_iff
theorem Affine.Simplex.affineSpan_pair_eq_altitude_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] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2))
(p : P),
affineSpan ℝ {p, s.points i} = s.altitude i ↔
p ≠ s.points i ∧
p ∈ affineSpan ℝ (Set.range s.points) ∧
p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' ↑(Finset.univ.erase i))).direction.orthogonal
This theorem states that for any normed additive commutative group `V`, any inner product space over the real numbers `ℝ` with `V` as the underlying set, any metric space `P`, and any normed additive torsor `P` over the group `V`, any natural number `n`, and any affine simplex `s` in `P` with `n + 1` points, for any vertex `i` of the simplex and any point `p`, the affine span of the set `{p, s.points i}` is equal to the altitude from `i` in the simplex `s` if and only if `p` is not equal to the `i`-th point of the simplex, `p` is in the affine span of the range of the points of the simplex, and the vector from the `i`-th point of the simplex to `p` is in the orthogonal complement of the direction of the affine span of the image of the set of all vertices of the simplex excluding `i`.
More concisely: For a normed additive commutative group `V`, an inner product space over `ℝ` with `V` as the underlying set, a metric space `P` with `V` as the underlying vector space, a normed additive torsor `P/V` over `V`, any simplex `s` in `P` with `n + 1` points, and any `i` and `p` such that `p` is not the `i`-th point of `s` and is in the affine span of `s.points` while lying in the orthogonal complement of the direction of the affine span of `s.points \ {i},` the affine span of `{p, s.points i}` equals the altitude from `i` in `s`.
|
Affine.Simplex.mongePoint_eq_of_range_eq
theorem Affine.Simplex.mongePoint_eq_of_range_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] {n : ℕ} {s₁ s₂ : Affine.Simplex ℝ P n},
Set.range s₁.points = Set.range s₂.points → s₁.mongePoint = s₂.mongePoint
This theorem states that for any two simplices `s₁` and `s₂` in a metric space, where their points are represented in a normed add torsor over an inner product space of normed add commutative groups, if the range of the points of `s₁` equals the range of the points of `s₂`, then the Monge point of `s₁` is equal to the Monge point of `s₂`. Here, the Monge point of a simplex, also known as the centroid or barycenter, is the average of its vertices. The range of a function, in this case `s₁.points` and `s₂.points`, is the set of all possible output values.
More concisely: In a metric space with points represented in a normed add torsor over an inner product space of normed add commutative groups, if two simplices have equal point sets, then their Monge points are equal.
|
Affine.Simplex.sum_mongePointVSubFaceCentroidWeightsWithCircumcenter
theorem Affine.Simplex.sum_mongePointVSubFaceCentroidWeightsWithCircumcenter :
∀ {n : ℕ} {i₁ i₂ : Fin (n + 3)},
i₁ ≠ i₂ →
(Finset.univ.sum fun i => Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i) = 0
This theorem states that, for any natural number `n` and any two distinct elements `i₁` and `i₂` of the set `Fin (n + 3)`, the sum over all elements of the universal set `Finset.univ` of the weights for the Monge point of an `(n+2)-simplex`, minus the centroid of an `n`-dimensional face, as defined by the function `Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter`, is equal to zero. This Monge point weight is given with respect to points of a simplex with a circumcenter, where the weights are defined differently depending on whether the point is a vertex (`pointIndex`) or circumcenter (`circumcenterIndex`).
More concisely: For any natural number `n` and distinct elements `i₁` and `i₂` of `Fin (n + 3)`, the sum of the weights of the Monge point of the `(n+2)`-simplex with respect to all elements of `Finset.univ`, minus the weights of the centroid of the `n`-dimensional face at `i₁` and `i₂`, equals zero.
|
Affine.Triangle.altitude_eq_mongePlane
theorem Affine.Triangle.altitude_eq_mongePlane :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → Affine.Simplex.altitude t i₁ = Affine.Simplex.mongePlane t i₂ i₃
The theorem `Affine.Triangle.altitude_eq_mongePlane` states that for any given triangle (formally, an instance of `Affine.Triangle ℝ P`), and for any three distinct indexes `i₁`, `i₂`, `i₃` from a 3-element finite set (`Fin 3`), the altitude of the triangle corresponding to the index `i₁` is equivalent to the Monge plane of the triangle corresponding to the indexes `i₂` and `i₃`. The triangle and its associated elements exist in a normed additive commutative group `V` and a metric space `P`, both having an inner product space over the real numbers and the latter being a normed additive torsor over `V`.
More concisely: For any triangle in a normed additive commutative group with an inner product and metric space over the real numbers, the altitude of one vertex is equivalent to the Monge plane formed by the other two vertices.
|
Affine.Triangle.dist_orthocenter_reflection_circumcenter
theorem Affine.Triangle.dist_orthocenter_reflection_circumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ : Fin 3},
i₁ ≠ i₂ →
dist t.orthocenter
((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (Affine.Simplex.circumcenter t)) =
Affine.Simplex.circumradius t
This theorem states that in an affine triangle (a collection of three affinely independent points), the distance from the orthocenter of the triangle to the reflection of the circumcenter in any side of the triangle equals the circumradius of the triangle. This is provided the two points defining the side (indexed by `i₁` and `i₂`) are distinct. Here, the orthocenter is the common intersection of the altitudes of the triangle, the circumcenter is the center of the circumscribing circle of the triangle, and the circumradius is the radius of this circumscribing circle.
More concisely: In an affine triangle with distinct sides defined by indices `i₁` and `i₂`, the distance from the orthocenter to the reflection of the circumcenter in side `[i₁, i₂]` equals the circumradius.
|
Affine.Simplex.sum_mongePointWeightsWithCircumcenter
theorem Affine.Simplex.sum_mongePointWeightsWithCircumcenter :
∀ (n : ℕ), (Finset.univ.sum fun i => Affine.Simplex.mongePointWeightsWithCircumcenter n i) = 1
This theorem states that the sum of the weights for the Monge point of an (n+2)-simplex, known as "mongePointWeightsWithCircumcenter", is always equal to 1. Here, the weights are calculated for all points in a finite set, which is implied by the assumption of the Fintype, and summed up. The weights are defined based on the index of the points with a circumcenter in the simplex, with different formulas used depending on whether the point is a regular point or the circumcenter of the simplex.
More concisely: The weights of the Monge point and all other points in an (n+2)-simplex, as defined by "mongePointWeightsWithCircumcenter," sum up to 1.
|
EuclideanGeometry.OrthocentricSystem.eq_insert_orthocenter
theorem EuclideanGeometry.OrthocentricSystem.eq_insert_orthocenter :
∀ {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 : Set P},
EuclideanGeometry.OrthocentricSystem s →
∀ {t : Affine.Triangle ℝ P}, Set.range t.points ⊆ s → s = insert t.orthocenter (Set.range t.points)
This theorem states that within any orthocentric system (a system composed of four points, three of which form a triangle and the fourth being the orthocenter of that triangle), given any triangle from that system, the fourth point of the system is the orthocenter of that triangle. It essentially tells us that in an orthocentric system, the set of points is equivalent to the union of the set of triangle's vertices and its orthocenter.
More concisely: In an orthocentric system, the orthocenter is a vertex of each triangle formed by three points in the system.
|
EuclideanGeometry.exists_of_range_subset_orthocentricSystem
theorem EuclideanGeometry.exists_of_range_subset_orthocentricSystem :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {t : Affine.Triangle ℝ P},
t.orthocenter ∉ Set.range t.points →
∀ {p : Fin 3 → P},
Set.range p ⊆ insert t.orthocenter (Set.range t.points) →
Function.Injective p →
(∃ i₁ i₂ i₃ j₂ j₃,
i₁ ≠ i₂ ∧
i₁ ≠ i₃ ∧
i₂ ≠ i₃ ∧
(∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
Set.range p = Set.range t.points
This theorem, named `EuclideanGeometry.exists_of_range_subset_orthocentricSystem`, states that given a triangle `t` in an orthocentric system (a system of four points, one of which is the orthocenter of the triangle formed by the other three), and three additional points `p` in the same system, one of two conditions must hold. Either we can find indices `i₁`, `i₂`, and `i₃` for `p` such that the point at index `i₁` is the orthocenter of `t`, and the points at indices `i₂` and `i₃` correspond to two distinct points of `t`, or the points of `p` are the same as the points of `t`. This is under the condition that the orthocenter of `t` does not belong to the set of points defining `t`, the set of points `p` is a subset of the set containing the orthocenter of `t` and the points of `t`, and the function mapping the indices to the points `p` is injective (meaning that each index maps to a unique point).
More concisely: In an orthocentric system, given a triangle with its orthocenter not in the triangle and a subset of four distinct points, either the triangle's orthocenter is one of the points, and the other two map to distinct triangle vertices, or all points are identical to the triangle's vertices.
|
Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub
theorem Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub :
∀ {n : ℕ} {i₁ i₂ : Fin (n + 3)},
i₁ ≠ i₂ →
Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ =
Affine.Simplex.mongePointWeightsWithCircumcenter n -
Affine.Simplex.centroidWeightsWithCircumcenter {i₁, i₂}ᶜ
The theorem `Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub` states that for any natural number `n` and any two different elements `i₁` and `i₂` of the finite set {0, 1, ..., n+2}, the function `mongePointVSubFaceCentroidWeightsWithCircumcenter` applied to `i₁` and `i₂`, which computes the weights for the Monge point of an (n+2)-simplex minus the centroid of an n-dimensional face, is equal to the result of subtracting the function `centroidWeightsWithCircumcenter` applied to the complement of the set `{i₁, i₂}` from the function `mongePointWeightsWithCircumcenter` applied to `n`. The latter two functions respectively compute the weights for the Monge point of an (n+2)-simplex and the centroid of some vertices of a simplex.
More concisely: For any natural number n and distinct elements i₁, i₂ of {0, 1, ..., n+2}, the weights of the Monge point of an (n+2)-simplex minus the centroid of an n-dimensional face at i₁, i₂, are equal to the weights of the Monge point of the entire simplex minus the centroid weights of the vertices in the complement of {i₁, i₂}.
|
Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter
theorem Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
s.mongePoint =
(↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ Finset.univ s.points -ᵥ s.circumcenter) +ᵥ s.circumcenter
This theorem states that for any n-dimensional simplex `s`, the Monge point of `s` is equal to the weighted average of the centroid of its vertices and its circumcenter. The weight applied to the vector from the circumcenter to the centroid is the ratio of `(n + 1)` to `(n - 1)`, where `n` is the dimension of the simplex. This theorem is defined in the context of a real inner product space.
More concisely: The Monge point of an n-dimensional simplex is the weighted average of its centroid and circumcenter, with weight `(n+1)/(n-1)` on the vector from the circumcenter to the centroid.
|
Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter
theorem Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P),
t.orthocenter =
3 • (Finset.centroid ℝ Finset.univ t.points -ᵥ Affine.Simplex.circumcenter t) +ᵥ
Affine.Simplex.circumcenter t
The theorem `Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter` states that for any real-valued affine triangle, the position of the orthocenter (the point where the triangle's altitudes intersect) can be calculated as three times the vector from the centroid (the average of the triangle's vertices) to the circumcenter (the center of the circle containing all vertices), added to the position of the circumcenter. This provides a geometric relationship between the orthocenter, centroid, and circumcenter of a triangle.
More concisely: The orthocenter of a real-valued affine triangle is three times the vector from the centroid to the circumcenter, plus the circumcenter's position.
|
EuclideanGeometry.affineSpan_of_orthocentricSystem
theorem EuclideanGeometry.affineSpan_of_orthocentricSystem :
∀ {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 : Set P},
EuclideanGeometry.OrthocentricSystem s →
∀ {p : Fin 3 → P}, Set.range p ⊆ s → Function.Injective p → affineSpan ℝ (Set.range p) = affineSpan ℝ s
This theorem is stating that in the context of Euclidean geometry, given an orthocentric system of points (which consists of the vertices of a triangle and its orthocenter), any three points from this system will span the same affine subspace as the entire orthocentric system. The conditions for this to hold are that the points must be within the orthocentric system, and that when mapped to the set of points `P` through a function, the function must be injective, meaning it distinctly maps every element of its domain to a unique element in its range. In other words, these three points are sufficient to define the entire system.
More concisely: In Euclidean geometry, any three points from an orthocentric system span the same affine subspace as the entire system, provided the mapping from the system to a set is injective.
|
Affine.Simplex.mongePlane_def
theorem Affine.Simplex.mongePlane_def :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2))
(i₁ i₂ : Fin (n + 3)),
s.mongePlane i₁ i₂ =
AffineSubspace.mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points)
(Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}).orthogonal ⊓
affineSpan ℝ (Set.range s.points)
This theorem defines a Monge plane in the context of affine simplices. Given a normed add commutative group `V`, an inner product space `V` over the real numbers, a metric space `P`, a normed add torsor `V` over `P`, a natural number `n`, an affine simplex `s` of dimension `n + 2` and two points `i₁` and `i₂` in the simplex, the Monge plane of `s` with respect to `i₁` and `i₂` is constructed as follows:
It is the intersection of two affine subspaces. The first affine subspace is constructed from the centroid of the set of points in the simplex excluding `i₁` and `i₂` (`Finset.centroid ℝ {i₁, i₂}ᶜ s.points`) and the orthogonal complement of the submodule spanned by the vector from point `i₂` to point `i₁` (`Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}`). The second affine subspace is the smallest affine subspace containing all the points in the simplex (`affineSpan ℝ (Set.range s.points)`).
More concisely: The Monge plane of an affine simplex in a normed add commutative group with respect to two points is the intersection of the affine subspace spanned by the simplex points and the orthogonal complement of the vector between the two points.
|
Affine.Triangle.affineSpan_orthocenter_point_le_altitude
theorem Affine.Triangle.affineSpan_orthocenter_point_le_altitude :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) (i : Fin 3),
affineSpan ℝ {t.orthocenter, t.points i} ≤ Affine.Simplex.altitude t i
The theorem `Affine.Triangle.affineSpan_orthocenter_point_le_altitude` states that for any triangle in an inner product space with a normed additively commutative group structure and a normed additive torsor structure, the affine span of its orthocenter and any of its vertices is contained within the corresponding altitude of the triangle. In other words, if you draw a line through the orthocenter and a vertex of the triangle, that line will be a subset of (or equal to) the line perpendicular to the opposite side passing through the same vertex, which is the definition of the altitude of the triangle at that vertex.
More concisely: The orthocenter of a triangle in an inner product space lies on or within the altitude of the triangle at that vertex.
|
Affine.Simplex.eq_mongePoint_of_forall_mem_mongePlane
theorem Affine.Simplex.eq_mongePoint_of_forall_mem_mongePlane :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} {s : Affine.Simplex ℝ P (n + 2)}
{i₁ : Fin (n + 3)} {p : P}, (∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂) → p = s.mongePoint
This theorem states that for any simplex in real affine space with an associated Monge point, if a point resides in all Monge planes pertaining to a particular vertex of the simplex, then the point must be the Monge point of the simplex. Specifically, this applies to an n-dimensional simplex in a normed add torsor over an inner product space on a metric space, where the underlying vector space is a normed add commutative group.
More concisely: In a normed add torsor over an inner product space on a metric space with an n-dimensional simplex and a vertex, if a point lies in all Monge planes associated with that vertex, then it is the Monge point of the simplex.
|
EuclideanGeometry.OrthocentricSystem.exists_circumradius_eq
theorem EuclideanGeometry.OrthocentricSystem.exists_circumradius_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 : Set P},
EuclideanGeometry.OrthocentricSystem s →
∃ r, ∀ (t : Affine.Triangle ℝ P), Set.range t.points ⊆ s → Affine.Simplex.circumradius t = r
This theorem states that for any Orthocentric System (a set of four points that consists of the vertices of a triangle and its orthocenter) in a given space, all triangles within this system have the same circumradius. More specifically, it asserts the existence of a real number 'r' such that for any triangle whose points are a subset of the orthocentric system, the circumradius of that triangle equals 'r'. This implies that all triangles formed by any combination of four points in the orthocentric system have congruent circumcircles.
More concisely: In an Orthocentric System, all triangles have the same circumradius.
|
Affine.Triangle.orthocenter_replace_orthocenter_eq_point
theorem Affine.Triangle.orthocenter_replace_orthocenter_eq_point :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {t₁ t₂ : Affine.Triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3},
i₁ ≠ i₂ →
i₁ ≠ i₃ →
i₂ ≠ i₃ →
j₁ ≠ j₂ →
j₁ ≠ j₃ →
j₂ ≠ j₃ →
t₂.points j₁ = t₁.orthocenter →
t₂.points j₂ = t₁.points i₂ → t₂.points j₃ = t₁.points i₃ → t₂.orthocenter = t₁.points i₁
The theorem `Affine.Triangle.orthocenter_replace_orthocenter_eq_point` states that for any two triangles `t1` and `t2` in an inner product space with a Normed Additive Commutative Group structure, if one of the vertices of `t1` is replaced by its orthocenter to form `t2` (where the vertices may not be listed in the same order), then the orthocenter of `t2` is the replaced vertex of `t1`. This is under the conditions that all points in both triangles are distinct and the corresponding points in `t2` are the orthocenter and two other points of `t1`. This theorem thus reflects a unique relationship between a triangle and another triangle formed by replacing one of its vertices with its orthocenter.
More concisely: For triangles in an inner product space with a Normed Additive Commutative Group structure, if one vertex of a triangle is replaced by its orthocenter and the other two vertices remain the same, then the new triangle has the same orthocenter as the original triangle.
|
Affine.Triangle.orthocenter_eq_mongePoint
theorem Affine.Triangle.orthocenter_eq_mongePoint :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P),
t.orthocenter = Affine.Simplex.mongePoint t
The theorem states that, for any Triangle `t` in an affine space over the real numbers, equipped with an inner product space structure and a metric space structure, the orthocenter of the triangle equals the Monge point of the triangle. Here, the orthocenter of a triangle is the common intersection of the lines perpendicular to the triangle's sides at their midpoints, while the Monge point of a triangle is a special point associated with the triangle in the context of projective geometry.
More concisely: The orthocenter and Monge point of a triangle in an affine space over the real numbers, with an inner product and metric structure, are equal.
|
Affine.Simplex.mongePoint_mem_mongePlane
theorem Affine.Simplex.mongePoint_mem_mongePlane :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2))
{i₁ i₂ : Fin (n + 3)}, s.mongePoint ∈ s.mongePlane i₁ i₂
This theorem states that for any normed additively commutative group `V`, any type `P`, given that `V` forms an inner product space over the real numbers, and `P` is a metric space with a normed additively commutative group structure, and for any natural number `n`, for any affine simplex `s` in `P` of dimension `n + 2`, and for any two indices `i₁` and `i₂` from `0` to `n + 2`, the Monge point of the simplex `s` lies in the Monge plane of the simplex `s` determined by the indices `i₁` and `i₂`.
More concisely: For any normed additively commutative group `V` forming an inner product space over the real numbers, any metric space `P` with a normed additively commutative group structure, and any affine simplex `s` in `P` of dimension `n+2`, the Monge point of `s` lies in the Monge plane of `s` determined by any two indices `i₁` and `i₂` from `0` to `n+2`.
|
Affine.Simplex.altitude_def
theorem Affine.Simplex.altitude_def :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1))
(i : Fin (n + 2)),
s.altitude i =
AffineSubspace.mk' (s.points i) (affineSpan ℝ (s.points '' ↑(Finset.univ.erase i))).direction.orthogonal ⊓
affineSpan ℝ (Set.range s.points)
The `Affine.Simplex.altitude_def` theorem provides the definition of an altitude in an affine simplex. For any normed additively commutative group `V`, any inner product space over `V`, any metric space `P`, any normed additive torsor `V P`, a natural number `n`, and an affine simplex `s` of dimension `n + 1` in `P`, the altitude from a given point `i` in the simplex is defined as the intersection of the affine subspace that is orthogonal to the affine span of the remaining points in the simplex (excluding the point `i`) and the affine span of all points in the simplex. The theorem essentially states that the altitude from any point in an affine simplex is a line perpendicular to the hyperplane formed by the other points in the simplex. The altitude is constructed from a point and a direction, in this case, the orthogonal direction to the affine span of the other points.
More concisely: The theorem defines the altitude of a point in an affine simplex as the line perpendicular to the affine hypeplane spanned by the other points, intersecting the affine span of all points in the simplex.
|
Affine.Triangle.altitude_replace_orthocenter_eq_affineSpan
theorem Affine.Triangle.altitude_replace_orthocenter_eq_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] {t₁ t₂ : Affine.Triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3},
i₁ ≠ i₂ →
i₁ ≠ i₃ →
i₂ ≠ i₃ →
j₁ ≠ j₂ →
j₁ ≠ j₃ →
j₂ ≠ j₃ →
t₂.points j₁ = t₁.orthocenter →
t₂.points j₂ = t₁.points i₂ →
t₂.points j₃ = t₁.points i₃ →
Affine.Simplex.altitude t₂ j₂ = affineSpan ℝ {t₁.points i₁, t₁.points i₂}
The theorem `Affine.Triangle.altitude_replace_orthocenter_eq_affineSpan` states the following mathematical fact in the context of affine geometry and triangles. Suppose we have a triangle, referred to as `t₁`, and we create a new triangle `t₂` by replacing one of the vertices of `t₁` with its orthocenter. Note that the vertices of `t₂` are not necessarily listed in the same order as `t₁`. The theorem then asserts that an altitude of `t₂` drawn from a vertex that was not replaced corresponds to the side of the original triangle `t₁`. More specifically, the affine span of this altitude is equal to the affine span of the points representing the original side in `t₁`. This claim is valid under the condition that all the vertices (represented by `i₁`, `i₂`, `i₃`, `j₁`, `j₂`, `j₃`) are distinct.
More concisely: The affine span of an altitude of a triangle with one vertex replaced by its orthocenter is equal to the affine span of the corresponding side in the original triangle, given that all vertices are distinct.
|
Affine.Triangle.orthocenter_mem_affineSpan
theorem Affine.Triangle.orthocenter_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] (t : Affine.Triangle ℝ P),
t.orthocenter ∈ affineSpan ℝ (Set.range t.points)
This theorem states that the orthocenter of a triangle lies within the affine span of the triangle's points. Specifically, given an affine triangle `t` defined in a normed add torsor and metric space, the orthocenter of `t` (denoted as `t.orthocenter`) is contained within the affine span of the set of points that define `t` (denoted as `Set.range t.points`). The underlying space is a normed add commutative group with an inner product space over real numbers.
More concisely: The orthocenter of a triangle in a normed add torsor and metric space lies in the affine span of the triangle's vertices.
|
Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter
theorem Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2))
{i₁ i₂ : Fin (n + 3)},
i₁ ≠ i₂ →
s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points =
(Finset.univ.weightedVSub s.pointsWithCircumcenter)
(Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂)
This theorem states that for an (n+2)-simplex, the vector difference between its Monge point and the centroid of an n-dimensional face, in terms of `pointsWithCircumcenter`, is equal to the weighted sum of vectors from `pointsWithCircumcenter` with weights specified by `mongePointVSubFaceCentroidWeightsWithCircumcenter` given two distinct vertices from the simplex. This equality holds in any inner product space over real numbers, with any affine coordinates and metric space structure. The simplex is defined by a set of (n+2) points in this metric space, and the n-dimensional face is specified by the set-complement of two specific (distinct) vertices of the simplex.
More concisely: In any inner product space over real numbers, the vector difference between a simplex's Monge point and the centroid of a chosen face is equal to the weighted sum of vectors from the simplex's circumcenter to the face's vertices, with weights defined by `mongePointVSubFaceCentroidWeightsWithCircumcenter`.
|
EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter
theorem EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {t : Affine.Triangle ℝ P},
t.orthocenter ∉ Set.range t.points →
∀ {p : Fin 3 → P},
Set.range p ⊆ insert t.orthocenter (Set.range t.points) →
Function.Injective p →
∃ c ∈ affineSpan ℝ (Set.range t.points), ∀ p₁ ∈ Set.range p, dist p₁ c = Affine.Simplex.circumradius t
This theorem states that for any three points in an orthocentric system created by a given triangle `t`, there exists a point in the affine span of the triangle such that its distance to all three points is equal to the circumradius of the triangle. The orthocentric system is defined in such a way that the orthocenter of the triangle is not one of the triangle's vertices. The points are uniquely identifiable and are included in the set formed by the orthocenter and the vertices of the triangle.
More concisely: In an orthocentric triangle, there exists a unique point in the affine hull that is equidistant to the triangle's orthocenter and its vertices, with this distance equal to the circumradius.
|
Affine.Simplex.direction_mongePlane
theorem Affine.Simplex.direction_mongePlane :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2))
{i₁ i₂ : Fin (n + 3)},
(s.mongePlane i₁ i₂).direction =
(Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}).orthogonal ⊓ vectorSpan ℝ (Set.range s.points)
The theorem `Affine.Simplex.direction_mongePlane` states that for a given Monge plane, defined on an (n+2)-simplex in an inner product space over the real numbers, the direction of this plane equals the intersection of the orthogonal complement of the span of the difference vector between two points `i₁` and `i₂` in the simplex, and the vector span of the set of all points in the simplex. In simpler words, the direction of the Monge plane is defined by the common elements in the orthogonal complement of the line between two points and the vector span of all points in the simplex.
More concisely: The direction of a Monge plane on an (n+2)-simplex in an inner product space over the real numbers is the intersection of the orthogonal complement of the difference between any two points in the simplex and the span of all points in the simplex.
|
Affine.Simplex.mongePoint_mem_affineSpan
theorem Affine.Simplex.mongePoint_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] {n : ℕ} (s : Affine.Simplex ℝ P n),
s.mongePoint ∈ affineSpan ℝ (Set.range s.points)
The theorem `Affine.Simplex.mongePoint_mem_affineSpan` states that for any affine simplex `s` of type `Affine.Simplex ℝ P n` where `V` is a normed add commutative group, `P` is a metric space, `V` is also an inner product space over the real numbers, and `P` is a normed add torsor over `V`, the Monge point of `s` lies in the affine span of the set of points of `s`. In simpler terms, the Monge point of any given simplex is always included in the smallest affine subspace that contains all the points of that simplex.
More concisely: The Monge point of an affine simplex in a normed add commutative group equipped with a metric and an inner product lies in its affine span.
|
Affine.Simplex.mem_altitude
theorem Affine.Simplex.mem_altitude :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1))
(i : Fin (n + 2)), s.points i ∈ s.altitude i
This theorem states that, for any given affine simplex of dimension `n+1`, any vertex of the simplex is contained in the corresponding altitude of the simplex. This is true for any normed additive commutative group `V`, inner product space over the reals `V`, metric space `P`, and normed additive torsor `V` over `P`. The altitude is defined with respect to the `i`-th vertex of the simplex, where `i` is a natural number less than or equal to `n+1`. In geometric terms, this means that if you draw a line from a vertex of a simplex perpendicular to the opposite face (the "altitude"), that vertex lies on the line.
More concisely: For any affine simplex of dimension `n+1` in a normed additive commutative group, inner product space over the reals, metric space, or normed additive torsor, each vertex lies on the altitude with respect to that vertex in the simplex.
|
Affine.Triangle.orthocenter_mem_altitude
theorem Affine.Triangle.orthocenter_mem_altitude :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ : Fin 3},
t.orthocenter ∈ Affine.Simplex.altitude t i₁
This theorem states that for any given affine triangle, which is a collection of three affinely independent points `t`, the orthocenter of this triangle is contained within the altitude of the triangle for any given index `i₁` in a 3-element finite set.
In more mathematically precise terms, an affine triangle is defined in a real number space `ℝ` with point type `P`, where `P` is a metric space and also a normed add torsor over a normed add comm group `V`. `V` is more specifically an inner product space over `ℝ`. The theorem then asserts that for any such defined triangle and a given index out of 3 possible indices (0, 1, 2 correspondingly to three vertices of the triangle), the orthocenter of the triangle belongs to the line of altitude emanating from the vertex indexed by `i₁`.
The orthocenter of a triangle is the common intersection of the lines dropped perpendicularly from a vertex to the opposite side (or the line extending the opposite side). An altitude of a triangle is the line segment drawn from a vertex of the triangle perpendicularly to the line containing the opposite side. Thus, this theorem is a formal mathematical confirmation of a commonly known geometric property of triangles.
More concisely: For any affine triangle in an inner product space, the orthocenter lies on the altitude of a vertex.
|
Affine.Simplex.direction_altitude
theorem Affine.Simplex.direction_altitude :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1))
(i : Fin (n + 2)),
(s.altitude i).direction =
(vectorSpan ℝ (s.points '' ↑(Finset.univ.erase i))).orthogonal ⊓ vectorSpan ℝ (Set.range s.points)
The theorem `Affine.Simplex.direction_altitude` states that for any given real-number affine simplex `s` of dimension `n + 1` and any index `i` in the finite set `{0, 1, ..., n+1}`, the direction of the altitude of the simplex `s` from the vertex specified by `i` is equal to the intersection of the orthogonal complement of the vector span of the set of differences of `s`'s points excluding the `i`-th point, and the vector span of the range of `s`'s points.
In other words, the direction of the altitude from a vertex of a simplex is perpendicular to the plane formed by the other vertices and lies within the span of the points defining the simplex.
More concisely: The direction of the altitude from a vertex of an affine simplex is the intersection of the orthogonal complement of the span of its non-including points and the span of all points.
|
Affine.Triangle.orthocenter_eq_of_range_eq
theorem Affine.Triangle.orthocenter_eq_of_range_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] {t₁ t₂ : Affine.Triangle ℝ P},
Set.range t₁.points = Set.range t₂.points → t₁.orthocenter = t₂.orthocenter
This theorem states that for any two triangles, identified as `t₁` and `t₂`, in a real number space with a specific set of algebraic properties (namely, it is a normed additively commutative group, inner product space, metric space, and normed additive torsor), if the set of points defining these triangles (obtained by the function `points`) are identical (i.e., `Set.range t₁.points = Set.range t₂.points`), then the orthocenters of these two triangles will also be the same (i.e., `t₁.orthocenter = t₂.orthocenter`).
In other words, in a geometrically and algebraically suitable space, if two triangles are defined by the same three points, their orthocenters (the common point of the lines perpendicular to the sides of the triangle passing through the corresponding opposite vertices) will be the same as well.
More concisely: In a normed additively commutative group, inner product space, metric space, and normed additive torsor, if two triangles have the same defining points, then they have the same orthocenters.
|