Monge point and orthocenter

This file defines the orthocenter of a triangle, via its n-dimensional generalization, the Monge point of a simplex.

Main definitions

• mongePoint is the Monge point of a simplex, defined in terms of its position on the Euler line and then shown to be the point of concurrence of the Monge planes.

• mongePlane is a Monge plane of an (n+2)-simplex, which is the (n+1)-dimensional affine subspace of the subspace spanned by the simplex that passes through the centroid of an n-dimensional face and is orthogonal to the opposite edge (in 2 dimensions, this is the same as an altitude).

• altitude is the line that passes through a vertex of a simplex and is orthogonal to the opposite face.

• orthocenter is defined, for the case of a triangle, to be the same as its Monge point, then shown to be the point of concurrence of the altitudes.

• OrthocentricSystem is a predicate on sets of points that says whether they are four points, one of which is the orthocenter of the other three (in which case various other properties hold, including that each is the orthocenter of the other three).

References

• https://en.wikipedia.org/wiki/Altitude_(triangle)
• https://en.wikipedia.org/wiki/Monge_point
• https://en.wikipedia.org/wiki/Orthocentric_system
• Małgorzata Buba-Brzozowa, The Monge Point and the 3(n+1) Point Sphere of an n-Simplex

def Affine.Simplex.mongePoint {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : P

The Monge point of a simplex (in 2 or more dimensions) is a generalization of the orthocenter of a triangle. It is defined to be the intersection of the Monge planes, where a Monge plane is the (n-1)-dimensional affine subspace of the subspace spanned by the simplex that passes through the centroid of an (n-2)-dimensional face and is orthogonal to the opposite edge (in 2 dimensions, this is the same as an altitude). The circumcenter O, centroid G and Monge point M are collinear in that order on the Euler line, with OG : GM = (n-1): 2. Here, we use that ratio to define the Monge point (so resulting in a point that equals the centroid in 0 or 1 dimensions), and then show in subsequent lemmas that the point so defined lies in the Monge planes and is their unique point of intersection.

theorem Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : Affine.Simplex.mongePoint s = (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ Finset.univ s.points -ᵥ Affine.Simplex.circumcenter s) +ᵥ Affine.Simplex.circumcenter s

The position of the Monge point in relation to the circumcenter and centroid.

theorem Affine.Simplex.mongePoint_mem_affineSpan {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) : Affine.Simplex.mongePoint s ∈ affineSpan ℝ (Set.range s.points)

The Monge point lies in the affine span.

theorem Affine.Simplex.mongePoint_eq_of_range_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {s₁ : Affine.Simplex ℝ P n} {s₂ : Affine.Simplex ℝ P n} (h : Set.range s₁.points = Set.range s₂.points) : Affine.Simplex.mongePoint s₁ = Affine.Simplex.mongePoint s₂

Two simplices with the same points have the same Monge point.

def Affine.Simplex.mongePointWeightsWithCircumcenter (n : ℕ) : Affine.Simplex.PointsWithCircumcenterIndex (n + 2) → ℝ

The weights for the Monge point of an (n+2)-simplex, in terms of pointsWithCircumcenter.

@[simp]

theorem Affine.Simplex.sum_mongePointWeightsWithCircumcenter (n : ℕ) : (Finset.sum Finset.univ fun i => Affine.Simplex.mongePointWeightsWithCircumcenter n i) = 1

mongePointWeightsWithCircumcenter sums to 1.

theorem Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) : Affine.Simplex.mongePoint s = ↑(Finset.affineCombination ℝ Finset.univ (Affine.Simplex.pointsWithCircumcenter s)) (Affine.Simplex.mongePointWeightsWithCircumcenter n)

The Monge point of an (n+2)-simplex, in terms of pointsWithCircumcenter.

def Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter {n : ℕ} (i₁ : Fin (n + 3)) (i₂ : Fin (n + 3)) : Affine.Simplex.PointsWithCircumcenterIndex (n + 2) → ℝ

The weights for the Monge point of an (n+2)-simplex, minus the centroid of an n-dimensional face, in terms of pointsWithCircumcenter. This definition is only valid when i₁ ≠ i₂.

theorem Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub {n : ℕ} {i₁ : Fin (n + 3)} {i₂ : Fin (n + 3)} (h : i₁ ≠ i₂) : Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ = Affine.Simplex.mongePointWeightsWithCircumcenter n - Affine.Simplex.centroidWeightsWithCircumcenter {i₁, i₂}ᶜ

mongePointVSubFaceCentroidWeightsWithCircumcenter is the result of subtracting centroidWeightsWithCircumcenter from mongePointWeightsWithCircumcenter.

@[simp]

theorem Affine.Simplex.sum_mongePointVSubFaceCentroidWeightsWithCircumcenter {n : ℕ} {i₁ : Fin (n + 3)} {i₂ : Fin (n + 3)} (h : i₁ ≠ i₂) : (Finset.sum Finset.univ fun i => Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i) = 0

mongePointVSubFaceCentroidWeightsWithCircumcenter sums to 0.

theorem Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) {i₁ : Fin (n + 3)} {i₂ : Fin (n + 3)} (h : i₁ ≠ i₂) : Affine.Simplex.mongePoint s -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points = ↑(Finset.weightedVSub Finset.univ (Affine.Simplex.pointsWithCircumcenter s)) (Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂)

The Monge point of an (n+2)-simplex, minus the centroid of an n-dimensional face, in terms of pointsWithCircumcenter.

theorem Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) {i₁ : Fin (n + 3)} {i₂ : Fin (n + 3)} : inner (Affine.Simplex.mongePoint s -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (Affine.Simplex.points s i₁ -ᵥ Affine.Simplex.points s i₂) = 0

The Monge point of an (n+2)-simplex, minus the centroid of an n-dimensional face, is orthogonal to the difference of the two vertices not in that face.

def Affine.Simplex.mongePlane {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) (i₁ : Fin (n + 3)) (i₂ : Fin (n + 3)) : AffineSubspace ℝ P

A Monge plane of an (n+2)-simplex is the (n+1)-dimensional affine subspace of the subspace spanned by the simplex that passes through the centroid of an n-dimensional face and is orthogonal to the opposite edge (in 2 dimensions, this is the same as an altitude). This definition is only intended to be used when i₁ ≠ i₂.

theorem Affine.Simplex.mongePlane_def {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) (i₁ : Fin (n + 3)) (i₂ : Fin (n + 3)) : Affine.Simplex.mongePlane s i₁ i₂ = AffineSubspace.mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (Submodule.span ℝ {Affine.Simplex.points s i₁ -ᵥ Affine.Simplex.points s i₂})ᗮ ⊓ affineSpan ℝ (Set.range s.points)

The definition of a Monge plane.

theorem Affine.Simplex.mongePlane_comm {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) (i₁ : Fin (n + 3)) (i₂ : Fin (n + 3)) : Affine.Simplex.mongePlane s i₁ i₂ = Affine.Simplex.mongePlane s i₂ i₁

The Monge plane associated with vertices i₁ and i₂ equals that associated with i₂ and i₁.

theorem Affine.Simplex.mongePoint_mem_mongePlane {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) {i₁ : Fin (n + 3)} {i₂ : Fin (n + 3)} : Affine.Simplex.mongePoint s ∈ Affine.Simplex.mongePlane s i₁ i₂

The Monge point lies in the Monge planes.

theorem Affine.Simplex.direction_mongePlane {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) {i₁ : Fin (n + 3)} {i₂ : Fin (n + 3)} : AffineSubspace.direction (Affine.Simplex.mongePlane s i₁ i₂) = (Submodule.span ℝ {Affine.Simplex.points s i₁ -ᵥ Affine.Simplex.points s i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

The direction of a Monge plane.

theorem Affine.Simplex.eq_mongePoint_of_forall_mem_mongePlane {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {s : Affine.Simplex ℝ P (n + 2)} {i₁ : Fin (n + 3)} {p : P} (h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ Affine.Simplex.mongePlane s i₁ i₂) : p = Affine.Simplex.mongePoint s

The Monge point is the only point in all the Monge planes from any one vertex.

def Affine.Simplex.altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : AffineSubspace ℝ P

An altitude of a simplex is the line that passes through a vertex and is orthogonal to the opposite face.

theorem Affine.Simplex.altitude_def {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : Affine.Simplex.altitude s i = AffineSubspace.mk' (Affine.Simplex.points s i) (AffineSubspace.direction (affineSpan ℝ (s.points '' ↑(Finset.erase Finset.univ i))))ᗮ ⊓ affineSpan ℝ (Set.range s.points)

The definition of an altitude.

theorem Affine.Simplex.mem_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : Affine.Simplex.points s i ∈ Affine.Simplex.altitude s i

A vertex lies in the corresponding altitude.

theorem Affine.Simplex.direction_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : AffineSubspace.direction (Affine.Simplex.altitude s i) = (vectorSpan ℝ (s.points '' ↑(Finset.erase Finset.univ i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

The direction of an altitude.

theorem Affine.Simplex.vectorSpan_isOrtho_altitude_direction {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : vectorSpan ℝ (s.points '' ↑(Finset.erase Finset.univ i)) ⟂ AffineSubspace.direction (Affine.Simplex.altitude s i)

The vector span of the opposite face lies in the direction orthogonal to an altitude.

instance Affine.Simplex.finiteDimensional_direction_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : FiniteDimensional ℝ { x // x ∈ AffineSubspace.direction (Affine.Simplex.altitude s i) }

An altitude is finite-dimensional.

@[simp]

theorem Affine.Simplex.finrank_direction_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : FiniteDimensional.finrank ℝ { x // x ∈ AffineSubspace.direction (Affine.Simplex.altitude s i) } = 1

An altitude is one-dimensional (i.e., a line).

theorem Affine.Simplex.affineSpan_pair_eq_altitude_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)) (i : Fin (n + 2)) (p : P) : affineSpan ℝ {p, Affine.Simplex.points s i} = Affine.Simplex.altitude s i ↔ p ≠ Affine.Simplex.points s i ∧ p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ Affine.Simplex.points s i ∈ (AffineSubspace.direction (affineSpan ℝ (s.points '' ↑(Finset.erase Finset.univ i))))ᗮ

A line through a vertex is the altitude through that vertex if and only if it is orthogonal to the opposite face.

def Affine.Triangle.orthocenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) : P

The orthocenter of a triangle is the intersection of its altitudes. It is defined here as the 2-dimensional case of the Monge point.

theorem Affine.Triangle.orthocenter_eq_mongePoint {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) : Affine.Triangle.orthocenter t = Affine.Simplex.mongePoint t

The orthocenter equals the Monge point.

theorem Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) : Affine.Triangle.orthocenter t = 3 • (Finset.centroid ℝ Finset.univ t.points -ᵥ Affine.Simplex.circumcenter t) +ᵥ Affine.Simplex.circumcenter t

The position of the orthocenter in relation to the circumcenter and centroid.

theorem Affine.Triangle.orthocenter_mem_affineSpan {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) : Affine.Triangle.orthocenter t ∈ affineSpan ℝ (Set.range t.points)

The orthocenter lies in the affine span.

theorem Affine.Triangle.orthocenter_eq_of_range_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {t₁ : Affine.Triangle ℝ P} {t₂ : Affine.Triangle ℝ P} (h : Set.range t₁.points = Set.range t₂.points) : Affine.Triangle.orthocenter t₁ = Affine.Triangle.orthocenter t₂

Two triangles with the same points have the same orthocenter.

theorem Affine.Triangle.altitude_eq_mongePlane {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Affine.Simplex.altitude t i₁ = Affine.Simplex.mongePlane t i₂ i₃

In the case of a triangle, altitudes are the same thing as Monge planes.

theorem Affine.Triangle.orthocenter_mem_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ : Fin 3} : Affine.Triangle.orthocenter t ∈ Affine.Simplex.altitude t i₁

The orthocenter lies in the altitudes.

theorem Affine.Triangle.eq_orthocenter_of_forall_mem_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {t : Affine.Triangle ℝ P} {i₁ : Fin 3} {i₂ : Fin 3} {p : P} (h₁₂ : i₁ ≠ i₂) (h₁ : p ∈ Affine.Simplex.altitude t i₁) (h₂ : p ∈ Affine.Simplex.altitude t i₂) : p = Affine.Triangle.orthocenter t

The orthocenter is the only point lying in any two of the altitudes.

theorem Affine.Triangle.dist_orthocenter_reflection_circumcenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ : Fin 3} {i₂ : Fin 3} (h : i₁ ≠ i₂) : dist (Affine.Triangle.orthocenter t) (↑(EuclideanGeometry.reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (Affine.Simplex.circumcenter t)) = Affine.Simplex.circumradius t

The distance from the orthocenter to the reflection of the circumcenter in a side equals the circumradius.

theorem Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ : Fin 3} {i₂ : Fin 3} (h : i₁ ≠ i₂) : dist (Affine.Triangle.orthocenter t) (↑(EuclideanGeometry.reflection (affineSpan ℝ (t.points '' ↑{i₁, i₂}))) (Affine.Simplex.circumcenter t)) = Affine.Simplex.circumradius t

The distance from the orthocenter to the reflection of the circumcenter in a side equals the circumradius, variant using a Finset.

theorem Affine.Triangle.affineSpan_orthocenter_point_le_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) (i : Fin 3) : affineSpan ℝ {Affine.Triangle.orthocenter t, Affine.Simplex.points t i} ≤ Affine.Simplex.altitude t i

The affine span of the orthocenter and a vertex is contained in the altitude.

theorem Affine.Triangle.altitude_replace_orthocenter_eq_affineSpan {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {t₁ : Affine.Triangle ℝ P} {t₂ : Affine.Triangle ℝ P} {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} {j₁ : Fin 3} {j₂ : Fin 3} {j₃ : Fin 3} (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) (hj₁₂ : j₁ ≠ j₂) (hj₁₃ : j₁ ≠ j₃) (hj₂₃ : j₂ ≠ j₃) (h₁ : Affine.Simplex.points t₂ j₁ = Affine.Triangle.orthocenter t₁) (h₂ : Affine.Simplex.points t₂ j₂ = Affine.Simplex.points t₁ i₂) (h₃ : Affine.Simplex.points t₂ j₃ = Affine.Simplex.points t₁ i₃) : Affine.Simplex.altitude t₂ j₂ = affineSpan ℝ {Affine.Simplex.points t₁ i₁, Affine.Simplex.points t₁ i₂}

Suppose we are given a triangle t₁, and replace one of its vertices by its orthocenter, yielding triangle t₂ (with vertices not necessarily listed in the same order). Then an altitude of t₂ from a vertex that was not replaced is the corresponding side of t₁.

theorem Affine.Triangle.orthocenter_replace_orthocenter_eq_point {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {t₁ : Affine.Triangle ℝ P} {t₂ : Affine.Triangle ℝ P} {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} {j₁ : Fin 3} {j₂ : Fin 3} {j₃ : Fin 3} (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) (hj₁₂ : j₁ ≠ j₂) (hj₁₃ : j₁ ≠ j₃) (hj₂₃ : j₂ ≠ j₃) (h₁ : Affine.Simplex.points t₂ j₁ = Affine.Triangle.orthocenter t₁) (h₂ : Affine.Simplex.points t₂ j₂ = Affine.Simplex.points t₁ i₂) (h₃ : Affine.Simplex.points t₂ j₃ = Affine.Simplex.points t₁ i₃) : Affine.Triangle.orthocenter t₂ = Affine.Simplex.points t₁ i₁

Suppose we are given a triangle t₁, and replace one of its vertices by its orthocenter, yielding triangle t₂ (with vertices not necessarily listed in the same order). Then the orthocenter of t₂ is the vertex of t₁ that was replaced.

def EuclideanGeometry.OrthocentricSystem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Set P) : Prop

Four points form an orthocentric system if they consist of the vertices of a triangle and its orthocenter.

theorem EuclideanGeometry.exists_of_range_subset_orthocentricSystem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {t : Affine.Triangle ℝ P} (ho : ¬Affine.Triangle.orthocenter t ∈ Set.range t.points) {p : Fin 3 → P} (hps : Set.range p ⊆ insert (Affine.Triangle.orthocenter t) (Set.range t.points)) (hpi : 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₁ = Affine.Triangle.orthocenter t ∧ j₂ ≠ j₃ ∧ Affine.Simplex.points t j₂ = p i₂ ∧ Affine.Simplex.points t j₃ = p i₃) ∨ Set.range p = Set.range t.points

This is an auxiliary lemma giving information about the relation of two triangles in an orthocentric system; it abstracts some reasoning, with no geometric content, that is common to some other lemmas. Suppose the orthocentric system is generated by triangle t, and we are given three points p in the orthocentric system. Then either we can find indices i₁, i₂ and i₃ for p such that p i₁ is the orthocenter of t and p i₂ and p i₃ are points j₂ and j₃ of t, or p has the same points as t.

theorem EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {t : Affine.Triangle ℝ P} (ho : ¬Affine.Triangle.orthocenter t ∈ Set.range t.points) {p : Fin 3 → P} (hps : Set.range p ⊆ insert (Affine.Triangle.orthocenter t) (Set.range t.points)) (hpi : Function.Injective p) : ∃ c, c ∈ affineSpan ℝ (Set.range t.points) ∧ ∀ (p₁ : P), p₁ ∈ Set.range p → dist p₁ c = Affine.Simplex.circumradius t

For any three points in an orthocentric system generated by triangle t, there is a point in the subspace spanned by the triangle from which the distance of all those three points equals the circumradius.

theorem EuclideanGeometry.OrthocentricSystem.affineIndependent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Set P} (ho : EuclideanGeometry.OrthocentricSystem s) {p : Fin 3 → P} (hps : Set.range p ⊆ s) (hpi : Function.Injective p) : AffineIndependent ℝ p

Any three points in an orthocentric system are affinely independent.

theorem EuclideanGeometry.affineSpan_of_orthocentricSystem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Set P} (ho : EuclideanGeometry.OrthocentricSystem s) {p : Fin 3 → P} (hps : Set.range p ⊆ s) (hpi : Function.Injective p) : affineSpan ℝ (Set.range p) = affineSpan ℝ s

Any three points in an orthocentric system span the same subspace as the whole orthocentric system.

theorem EuclideanGeometry.OrthocentricSystem.exists_circumradius_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Set P} (ho : EuclideanGeometry.OrthocentricSystem s) : ∃ r, ∀ (t : Affine.Triangle ℝ P), Set.range t.points ⊆ s → Affine.Simplex.circumradius t = r

All triangles in an orthocentric system have the same circumradius.

theorem EuclideanGeometry.OrthocentricSystem.eq_insert_orthocenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Set P} (ho : EuclideanGeometry.OrthocentricSystem s) {t : Affine.Triangle ℝ P} (ht : Set.range t.points ⊆ s) : s = insert (Affine.Triangle.orthocenter t) (Set.range t.points)

Given any triangle in an orthocentric system, the fourth point is its orthocenter.