geometry.euclidean.monge_point

source

noncomputable def affine.simplex.monge_point {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor 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.

Equations

s.monge_point = (↑(n + 1) / ↑(n - 1)) • (finset.centroid ℝ finset.univ s.points -ᵥ s.circumcenter) +ᵥ s.circumcenter

source

theorem affine.simplex.monge_point_eq_smul_vsub_vadd_circumcenter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P n) :

s.monge_point = (↑(n + 1) / ↑(n - 1)) • (finset.centroid ℝ finset.univ s.points -ᵥ s.circumcenter) +ᵥ s.circumcenter

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

source

theorem affine.simplex.monge_point_mem_affine_span {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P n) :

s.monge_point ∈ affine_span ℝ (set.range s.points)

The Monge point lies in the affine span.

source

theorem affine.simplex.monge_point_eq_of_range_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} {s₁ s₂ : affine.simplex ℝ P n} (h : set.range s₁.points = set.range s₂.points) :

s₁.monge_point = s₂.monge_point

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

source

noncomputable def affine.simplex.monge_point_weights_with_circumcenter (n : ℕ) :

affine.simplex.points_with_circumcenter_index (n + 2) → ℝ

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

Equations

source

@[simp]

theorem affine.simplex.sum_monge_point_weights_with_circumcenter (n : ℕ) :

finset.univ.sum (λ (i : affine.simplex.points_with_circumcenter_index (n + 2)), affine.simplex.monge_point_weights_with_circumcenter n i) = 1

monge_point_weights_with_circumcenter sums to 1.

source

theorem affine.simplex.monge_point_eq_affine_combination_of_points_with_circumcenter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) :

s.monge_point = ⇑(finset.affine_combination ℝ finset.univ s.points_with_circumcenter) (affine.simplex.monge_point_weights_with_circumcenter n)

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

source

noncomputable def affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter {n : ℕ} (i₁ i₂ : fin (n + 3)) :

affine.simplex.points_with_circumcenter_index (n + 2) → ℝ

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

Equations

affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂ affine.simplex.points_with_circumcenter_index.circumcenter_index = (-2) / ↑(n + 1)
affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂ (affine.simplex.points_with_circumcenter_index.point_index i) = ite (i = i₁ ∨ i = i₂) (↑(n + 1))⁻¹ 0

source

theorem affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter_eq_sub {n : ℕ} {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) :

affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂ = affine.simplex.monge_point_weights_with_circumcenter n - affine.simplex.centroid_weights_with_circumcenter {i₁, i₂}ᶜ

monge_point_vsub_face_centroid_weights_with_circumcenter is the result of subtracting centroid_weights_with_circumcenter from monge_point_weights_with_circumcenter.

source

@[simp]

theorem affine.simplex.sum_monge_point_vsub_face_centroid_weights_with_circumcenter {n : ℕ} {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) :

finset.univ.sum (λ (i : affine.simplex.points_with_circumcenter_index (n + 2)), affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂ i) = 0

monge_point_vsub_face_centroid_weights_with_circumcenter sums to 0.

source

theorem affine.simplex.monge_point_vsub_face_centroid_eq_weighted_vsub_of_points_with_circumcenter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) :

s.monge_point -ᵥ finset.centroid ℝ {i₁, i₂}ᶜ s.points = ⇑(finset.univ.weighted_vsub s.points_with_circumcenter) (affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂)

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

source

theorem affine.simplex.inner_monge_point_vsub_face_centroid_vsub {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) {i₁ i₂ : fin (n + 3)} :

has_inner.inner (s.monge_point -ᵥ finset.centroid ℝ {i₁, i₂}ᶜ s.points) (s.points i₁ -ᵥ s.points 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.

source

noncomputable def affine.simplex.monge_plane {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) (i₁ i₂ : fin (n + 3)) :

affine_subspace ℝ 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₂.

Equations

s.monge_plane i₁ i₂ = affine_subspace.mk' (finset.centroid ℝ {i₁, i₂}ᶜ s.points) (Span {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ affine_span ℝ (set.range s.points)

source

theorem affine.simplex.monge_plane_def {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) (i₁ i₂ : fin (n + 3)) :

s.monge_plane i₁ i₂ = affine_subspace.mk' (finset.centroid ℝ {i₁, i₂}ᶜ s.points) (Span {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ affine_span ℝ (set.range s.points)

The definition of a Monge plane.

source

theorem affine.simplex.monge_plane_comm {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) (i₁ i₂ : fin (n + 3)) :

s.monge_plane i₁ i₂ = s.monge_plane i₂ i₁

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

source

theorem affine.simplex.monge_point_mem_monge_plane {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) {i₁ i₂ : fin (n + 3)} :

s.monge_point ∈ s.monge_plane i₁ i₂

The Monge point lies in the Monge planes.

source

theorem affine.simplex.direction_monge_plane {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) {i₁ i₂ : fin (n + 3)} :

(s.monge_plane i₁ i₂).direction = (Span {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vector_span ℝ (set.range s.points)

The direction of a Monge plane.

source

theorem affine.simplex.eq_monge_point_of_forall_mem_monge_plane {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} {s : affine.simplex ℝ P (n + 2)} {i₁ : fin (n + 3)} {p : P} (h : ∀ (i₂ : fin (n + 3)), i₁ ≠ i₂ → p ∈ s.monge_plane i₁ i₂) :

p = s.monge_point

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

source

noncomputable def affine.simplex.altitude {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

affine_subspace ℝ P

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

Equations

s.altitude i = affine_subspace.mk' (s.points i) ((affine_span ℝ (s.points '' ↑(finset.univ.erase i))).direction)ᗮ ⊓ affine_span ℝ (set.range s.points)

source

theorem affine.simplex.altitude_def {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

s.altitude i = affine_subspace.mk' (s.points i) ((affine_span ℝ (s.points '' ↑(finset.univ.erase i))).direction)ᗮ ⊓ affine_span ℝ (set.range s.points)

The definition of an altitude.

source

theorem affine.simplex.mem_altitude {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

s.points i ∈ s.altitude i

A vertex lies in the corresponding altitude.

source

theorem affine.simplex.direction_altitude {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

(s.altitude i).direction = (vector_span ℝ (s.points '' ↑(finset.univ.erase i)))ᗮ ⊓ vector_span ℝ (set.range s.points)

The direction of an altitude.

source

theorem affine.simplex.vector_span_is_ortho_altitude_direction {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

vector_span ℝ (s.points '' ↑(finset.univ.erase i)) ⟂ (s.altitude i).direction

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

source

@[protected, instance]

def affine.simplex.finite_dimensional_direction_altitude {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

finite_dimensional ℝ ↥((s.altitude i).direction)

An altitude is finite-dimensional.

source

@[simp]

theorem affine.simplex.finrank_direction_altitude {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

fdim ↥((s.altitude i).direction) = 1

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

source

theorem affine.simplex.affine_span_pair_eq_altitude_iff {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) (p : P) :

affine_span ℝ {p, s.points i} = s.altitude i ↔ p ≠ s.points i ∧ p ∈ affine_span ℝ (set.range s.points) ∧ p -ᵥ s.points i ∈ ((affine_span ℝ (s.points '' ↑(finset.univ.erase i))).direction)ᗮ

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

source

noncomputable def affine.triangle.orthocenter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor 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.

Equations

t.orthocenter = affine.simplex.monge_point t

source

theorem affine.triangle.orthocenter_eq_monge_point {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) :

t.orthocenter = affine.simplex.monge_point t

The orthocenter equals the Monge point.

source

theorem affine.triangle.orthocenter_eq_smul_vsub_vadd_circumcenter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) :

t.orthocenter = 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.

source

theorem affine.triangle.orthocenter_mem_affine_span {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) :

t.orthocenter ∈ affine_span ℝ (set.range t.points)

The orthocenter lies in the affine span.

source

theorem affine.triangle.orthocenter_eq_of_range_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {t₁ t₂ : affine.triangle ℝ P} (h : set.range t₁.points = set.range t₂.points) :

t₁.orthocenter = t₂.orthocenter

Two triangles with the same points have the same orthocenter.

source

theorem affine.triangle.altitude_eq_monge_plane {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :

affine.simplex.altitude t i₁ = affine.simplex.monge_plane t i₂ i₃

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

source

theorem affine.triangle.orthocenter_mem_altitude {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) {i₁ : fin 3} :

t.orthocenter ∈ affine.simplex.altitude t i₁

The orthocenter lies in the altitudes.

source

theorem affine.triangle.eq_orthocenter_of_forall_mem_altitude {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {t : affine.triangle ℝ P} {i₁ i₂ : fin 3} {p : P} (h₁₂ : i₁ ≠ i₂) (h₁ : p ∈ affine.simplex.altitude t i₁) (h₂ : p ∈ affine.simplex.altitude t i₂) :

p = t.orthocenter

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

source

theorem affine.triangle.dist_orthocenter_reflection_circumcenter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) {i₁ i₂ : fin 3} (h : i₁ ≠ i₂) :

has_dist.dist t.orthocenter (⇑(euclidean_geometry.reflection (affine_span ℝ (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.

source

theorem affine.triangle.dist_orthocenter_reflection_circumcenter_finset {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) {i₁ i₂ : fin 3} (h : i₁ ≠ i₂) :

has_dist.dist t.orthocenter (⇑(euclidean_geometry.reflection (affine_span ℝ (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.

source

theorem affine.triangle.affine_span_orthocenter_point_le_altitude {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) (i : fin 3) :

affine_span ℝ {t.orthocenter, t.points i} ≤ affine.simplex.altitude t i

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

source

theorem affine.triangle.altitude_replace_orthocenter_eq_affine_span {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {t₁ t₂ : affine.triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : fin 3} (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) (hj₁₂ : j₁ ≠ j₂) (hj₁₃ : j₁ ≠ j₃) (hj₂₃ : j₂ ≠ j₃) (h₁ : t₂.points j₁ = t₁.orthocenter) (h₂ : t₂.points j₂ = t₁.points i₂) (h₃ : t₂.points j₃ = t₁.points i₃) :

affine.simplex.altitude t₂ j₂ = affine_span ℝ {t₁.points i₁, t₁.points 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₁.

source

theorem affine.triangle.orthocenter_replace_orthocenter_eq_point {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {t₁ t₂ : affine.triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : fin 3} (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) (hj₁₂ : j₁ ≠ j₂) (hj₁₃ : j₁ ≠ j₃) (hj₂₃ : j₂ ≠ j₃) (h₁ : t₂.points j₁ = t₁.orthocenter) (h₂ : t₂.points j₂ = t₁.points i₂) (h₃ : t₂.points j₃ = t₁.points i₃) :

t₂.orthocenter = t₁.points 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.

source

def euclidean_geometry.orthocentric_system {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : set P) :

Prop

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

Equations

euclidean_geometry.orthocentric_system s = ∃ (t : affine.triangle ℝ P), t.orthocenter ∉ set.range t.points ∧ s = has_insert.insert t.orthocenter (set.range t.points)

source

theorem euclidean_geometry.exists_of_range_subset_orthocentric_system {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {t : affine.triangle ℝ P} (ho : t.orthocenter ∉ set.range t.points) {p : fin 3 → P} (hps : set.range p ⊆ has_insert.insert t.orthocenter (set.range t.points)) (hpi : function.injective p) :

(∃ (i₁ i₂ i₃ j₂ j₃ : fin 3), 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 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.

source

theorem euclidean_geometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {t : affine.triangle ℝ P} (ho : t.orthocenter ∉ set.range t.points) {p : fin 3 → P} (hps : set.range p ⊆ has_insert.insert t.orthocenter (set.range t.points)) (hpi : function.injective p) :

∃ (c : P) (H : c ∈ affine_span ℝ (set.range t.points)), ∀ (p₁ : P), p₁ ∈ set.range p → has_dist.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.

source

theorem euclidean_geometry.orthocentric_system.affine_independent {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : set P} (ho : euclidean_geometry.orthocentric_system s) {p : fin 3 → P} (hps : set.range p ⊆ s) (hpi : function.injective p) :

affine_independent ℝ p

Any three points in an orthocentric system are affinely independent.

source

theorem euclidean_geometry.affine_span_of_orthocentric_system {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : set P} (ho : euclidean_geometry.orthocentric_system s) {p : fin 3 → P} (hps : set.range p ⊆ s) (hpi : function.injective p) :

affine_span ℝ (set.range p) = affine_span ℝ s

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

source

theorem euclidean_geometry.orthocentric_system.exists_circumradius_eq {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : set P} (ho : euclidean_geometry.orthocentric_system 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.

source

theorem euclidean_geometry.orthocentric_system.eq_insert_orthocenter {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : set P} (ho : euclidean_geometry.orthocentric_system s) {t : affine.triangle ℝ P} (ht : set.range t.points ⊆ s) :

s = has_insert.insert t.orthocenter (set.range t.points)

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

mathlib3 documentation

Monge point and orthocenter #

Main definitions #

References #