Theorems · Theorem · geometry

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 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.

Defined in

Mathlib.Geometry.Euclidean.MongePoint

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor