English
There is a closed form expressing secondInter as a line map with a particular fractional coefficient.
Русский
Существует явное выражение secondInter через линейное отображение линии с определённым дробным коэффициентом.
LaTeX
$$$s.secondInter(p, p' - p) = \\text{AffineMap.lineMap}(p,p')(-2 \\frac{\\langle p' - p, p - s.center\\rangle}{\\langle p' - p, p' - p\\rangle})$$$
Lean4
/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, and the second point is not outside the sphere, the second point is weakly
between the first point and the result of `secondInter`. -/
theorem wbtw_secondInter {s : Sphere P} {p p' : P} (hp : p ∈ s) (hp' : dist p' s.center ≤ s.radius) :
Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p)) := by
by_cases h : p' = p; · simp [h]
refine
wbtw_of_collinear_of_dist_center_le_radius (s.secondInter_collinear p p') hp hp' ((Sphere.secondInter_mem _).2 hp)
?_
intro he
rw [eq_comm, Sphere.secondInter_eq_self_iff, ← neg_neg (p' -ᵥ p), inner_neg_left, neg_vsub_eq_vsub_rev, neg_eq_zero,
eq_comm] at he
exact ((inner_pos_or_eq_of_dist_le_radius hp hp').resolve_right (Ne.symm h)).ne he
