English
For a point p on a sphere and a line through p spanned by v, any p' on this line is either p or s.secondInter p v, provided p' lies on the sphere.
Русский
Для точки p на сфере и прямой через p порождённой вектора v, любая точка p' на этой прямой — либо p, либо s.secondInter p v, если p' лежит на сфере.
LaTeX
$$$p' = p \\lor p' = s.secondInter(p,v) \\iff p' \\in s$$$
Lean4
/-- A point on a line through a point on a sphere equals that point or `secondInter`. -/
theorem eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem {s : Sphere P} {p : P} (hp : p ∈ s) {v : V} {p' : P}
(hp' : p' ∈ AffineSubspace.mk' p (ℝ ∙ v)) : p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s :=
by
refine ⟨fun h => ?_, fun h => ?_⟩
· rcases h with (h | h)
· rwa [h]
· rwa [h, Sphere.secondInter_mem]
· rw [AffineSubspace.mem_mk', Submodule.mem_span_singleton] at hp'
rcases hp' with ⟨r, hr⟩
rw [eq_comm, ← eq_vadd_iff_vsub_eq] at hr
subst hr
by_cases hv : v = 0
· simp [hv]
rw [Sphere.secondInter]
rw [mem_sphere] at h hp
rw [← hp, dist_smul_vadd_eq_dist _ _ hv] at h
rcases h with (h | h) <;> simp [h]
