English
For a sphere s and as, the equality dist(center, orthogonalProjection(as, center)) = radius is equivalent to s.IsTangentAt(orthogonalProjection(as, center)) as.
Русский
Равенство dist(center, orthogonalProjection(as, center)) = radius эквивалентно IsTangentAt(orthogonalProjection(as, center)) как.
LaTeX
$$$ \\operatorname{dist}(s.center, \\operatorname{orthogonalProjection}(as, s.center)) = s.radius \\iff s.IsTangentAt (\\operatorname{orthogonalProjection}(as, s.center)) as $$$
Lean4
theorem dist_orthogonalProjection_eq_radius_iff_isTangentAt {s : Sphere P} {as : AffineSubspace ℝ P} [Nonempty as]
[as.direction.HasOrthogonalProjection] :
dist s.center (orthogonalProjection as s.center) = s.radius ↔ s.IsTangentAt (orthogonalProjection as s.center) as :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· refine ⟨?_, orthogonalProjection_mem _, fun p hp ↦ ?_⟩
· rwa [mem_sphere']
· rw [SetLike.mem_coe, mem_orthRadius_iff_inner_left]
exact
orthogonalProjection_vsub_mem_direction_orthogonal as s.center _
(vsub_orthogonalProjection_mem_direction s.center hp)
· rw [dist_orthogonalProjection_eq_infDist, h.isTangent.infDist_eq_radius]
