English
Let s be a cospherical subset of a space P. For any injective map p from the 3-point index set into P whose range lies in s, the three points p(0), p(1), p(2) are affinely independent over the real numbers.
Русский
Пусть s — кососферное подмножество пространства P. Для любой инъекции p: Fin(3) → P, чья область значений лежит в s, тройка точек p(0), p(1), p(2) аффinely независима над ℝ.
LaTeX
$$$\forall s\subseteq P,\ Cospherical(s)\Rightarrow\forall p:\mathrm{Fin}(3)\to P,\mathrm{range}(p)\subseteq s \Rightarrow\mathrm{Injective}(p)\Rightarrow\mathrm{AffineIndependent}_{\mathbb{R}}(p)$$$
Lean4
/-- Any three points in a cospherical set are affinely independent. -/
theorem affineIndependent {s : Set P} (hs : Cospherical s) {p : Fin 3 → P} (hps : Set.range p ⊆ s)
(hpi : Function.Injective p) : AffineIndependent ℝ p :=
by
rw [affineIndependent_iff_not_collinear]
intro hc
rw [collinear_iff_of_mem (Set.mem_range_self (0 : Fin 3))] at hc
rcases hc with ⟨v, hv⟩
rw [Set.forall_mem_range] at hv
have hv0 : v ≠ 0 := by
intro h
have he : p 1 = p 0 := by simpa [h] using hv 1
exact (by decide : (1 : Fin 3) ≠ 0) (hpi he)
rcases hs with ⟨c, r, hs⟩
have hs' := fun i => hs (p i) (Set.mem_of_mem_of_subset (Set.mem_range_self _) hps)
choose f hf using hv
have hsd : ∀ i, dist (f i • v +ᵥ p 0) c = r := by
intro i
rw [← hf]
exact hs' i
have hf0 : f 0 = 0 := by
have hf0' := hf 0
rw [eq_comm, ← @vsub_eq_zero_iff_eq V, vadd_vsub, smul_eq_zero] at hf0'
simpa [hv0] using hf0'
have hfi : Function.Injective f := by
intro i j h
have hi := hf i
rw [h, ← hf j] at hi
exact hpi hi
simp_rw [← hsd 0, hf0, zero_smul, zero_vadd, dist_smul_vadd_eq_dist (p 0) c hv0] at hsd
have hfn0 : ∀ i, i ≠ 0 → f i ≠ 0 := fun i => (hfi.ne_iff' hf0).2
have hfn0' : ∀ i, i ≠ 0 → f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫ :=
by
intro i hi
have hsdi := hsd i
simpa [hfn0, hi] using hsdi
have hf12 : f 1 = f 2 := by rw [hfn0' 1 (by decide), hfn0' 2 (by decide)]
exact (by decide : (1 : Fin 3) ≠ 2) (hfi hf12)
