existsUnique_dist_eq — Mathlib

English

Given a finite nonempty affinely independent family of points p:ι → P in a Euclidean space, there exists a unique circumsphere for these points; i.e., there is a unique center in the affine span of the vertices that contains all the points inside the circumsphere.

Русский

Пусть дано конечное непустое афинно независимое семейство точек p:ι → P. Существуют единственная циркумсфера, центр которой лежит в афинном охвате вершин и которая содержит все вершины.

LaTeX

$$$\\forall ι\\;[hne : Nonempty ι]\\[Finite ι]\\; (p: ι \\to P)\\; \\text{AffineIndependent}(\\mathbb{R},p) \\Rightarrow \\exists! cs:\\ Sphere P,\\; cs.center \\in affineSpan ℝ (Set.range p) \\land Set.range p \\subset cs.$$$

Lean4

/-- Given a finite nonempty affinely independent family of points,
there is a unique (circumcenter, circumradius) pair for those points
in the affine subspace they span. -/
theorem _root_.AffineIndependent.existsUnique_dist_eq {ι : Type*} [hne : Nonempty ι] [Finite ι] {p : ι → P}
    (ha : AffineIndependent ℝ p) :
    ∃! cs : Sphere P, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ (cs : Set P) :=
  by
  cases nonempty_fintype ι
  induction hn : Fintype.card ι generalizing ι with
  | zero =>
    exfalso
    have h := Fintype.card_pos_iff.2 hne
    cutsat
  | succ m hm =>
    rcases m with - | m
    · rw [Fintype.card_eq_one_iff] at hn
      obtain ⟨i, hi⟩ := hn
      haveI : Unique ι := ⟨⟨i⟩, hi⟩
      use ⟨p i, 0⟩
      simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton]
      constructor
      · simp_rw [hi default, Set.singleton_subset_iff]
        exact ⟨⟨⟩, by simp only [Metric.sphere_zero, Set.mem_singleton_iff]⟩
      · rintro ⟨cc, cr⟩
        rintro ⟨rfl, hdist⟩
        replace hdist : 0 = cr := by simpa using hdist
        rw [hi default, hdist]
    · have i := hne.some
      let ι2 := { x // x ≠ i }
      classical
      have hc : Fintype.card ι2 = m + 1 :=
        by
        rw [Fintype.card_of_subtype {x | x ≠ i}]
        · rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _), Finset.card_sdiff, Finset.card_univ,
            hn]
          simp
        · simp
      haveI : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
      have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
      replace hm := hm ha2 _ hc
      have hr : Set.range p = insert (p i) (Set.range fun i2 : ι2 => p i2) :=
        by
        change _ = insert _ (Set.range fun i2 : {x | x ≠ i} => p i2)
        rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
        congr with j
        simp [Classical.em]
      rw [hr, ← affineSpan_insert_affineSpan]
      refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
      convert ha.notMem_affineSpan_diff i Set.univ
      change (Set.range fun i2 : {x | x ≠ i} => p i2) = _
      rw [← Set.image_eq_range]
      congr 1 with j
      simp

Похожие утверждения