Theorems · Theorem · geometry

EuclideanGeometry.existsUnique_dist_eq_of_insert

∀ {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} [s.direction.HasOrthogonalProjection] {ps : Set P},
  ps.Nonempty →
    ∀ {p : P},
      ps ⊆ ↑s →
        p ∉ s →
          (∃! cs, cs.center ∈ s ∧ ps ⊆ Metric.sphere cs.center cs.radius) →
            ∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius

The induction step for the existence and uniqueness of the circumcenter. Given a nonempty set of points in a nonempty affine subspace whose direction is complete, such that there is a unique (circumcenter, circumradius) pair for those points in that subspace, and a point p not in that subspace, there is a unique (circumcenter, circumradius) pair for the set with p added, in the span of the subspace with p added.

Defined in

Mathlib.Geometry.Euclidean.Circumcenter

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorSubmodule.HasOrthogonalProjection