Theorems · Theorem · geometry

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

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.

Defined in

Mathlib.Geometry.Euclidean.MongePoint

Cited by

2 results in Mathlib

Foundations

Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor