Theorems · Theorem · geometry

EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two

∀ {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 : AffineSubspace ℝ P} [FiniteDimensional ℝ ↥s.direction],
  Module.finrank ℝ ↥s.direction = 2 →
    ∀ {c₁ c₂ p₁ p₂ p : P},
      c₁ ∈ s →
        c₂ ∈ s →
          p₁ ∈ s →
            p₂ ∈ s →
              p ∈ s →
                ∀ {r₁ r₂ : ℝ},
                  c₁ ≠ c₂ →
                    p₁ ≠ p₂ →
                      dist p₁ c₁ = r₁ →
                        dist p₂ c₁ = r₁ →
                          dist p c₁ = r₁ → dist p₁ c₂ = r₂ → dist p₂ c₂ = r₂ → dist p c₂ = r₂ → p = p₁ ∨ p = p₂

Distances r₁ r₂ of p from two different points c₁ c₂ determine at most two points p₁ p₂ in a two-dimensional subspace containing those points (two circles intersect in at most two points).

Defined in

Mathlib.Geometry.Euclidean.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFiniteDimensional