English
If ∠ q p s.center = π/2 and p ∈ s, then the line pq is tangent to s at p.
Русский
Если ∠ q p s.center = π/2 и p лежит на сфере s, то прямая pq касается сферы в p.
LaTeX
$$$\\angle q p s.center = \\dfrac{\\pi}{2} \\land p \\in s \\Rightarrow s.IsTangentAt(p, line(p,q))$$$
Lean4
/-- If the angle between the line `p q` and the radius at `p` equals `π / 2`, then the line `p q` is
tangent to the sphere at `p`. -/
theorem IsTangentAt_of_angle_eq_pi_div_two {s : Sphere P} {p q : P} (h : ∠ q p s.center = π / 2) (hp : p ∈ s) :
s.IsTangentAt p line[ℝ, p, q] := by
have hp_mem := left_mem_affineSpan_pair ℝ p q
refine ⟨hp, hp_mem, ?_⟩
have h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0 := by
rwa [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, ← neg_vsub_eq_vsub_rev p s.center, inner_neg_right,
neg_eq_zero] at h
have hq : q ∈ s.orthRadius p := by simp [Sphere.mem_orthRadius_iff_inner_left, h_ortho]
rw [affineSpan_le]
have hp : p ∈ s.orthRadius p := by simp [Sphere.self_mem_orthRadius]
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
exact ⟨hp, hq⟩
