angle_eq_pi_div_two — Mathlib

English

If the angle at p between q and the center of sphere s is π/2, then the line through p and q is tangent to s.

Русский

Если угол q-po-centre-s равен π/2, то прямая через p и q касается сферы в точке p.

LaTeX

$$$\\angle q p s.center = \\dfrac{\\pi}{2} \\quad\\Rightarrow\\quad s.IsTangentAt(p,\\ line_{\\mathbb{R}}(p,q))$$$

Lean4

/-- For a tangent line to a sphere, the angle between the line and the radius at the tangent point
equals `π / 2`. -/
theorem angle_eq_pi_div_two {s : Sphere P} {p q : P} {as : AffineSubspace ℝ P} (h : s.IsTangentAt p as)
    (hq_mem : q ∈ as) : ∠ q p s.center = π / 2 :=
  by
  have h1 := IsTangentAt.inner_left_eq_zero_of_mem h hq_mem
  rw [inner_eq_zero_iff_angle_eq_pi_div_two] at h1
  rw [angle, ← neg_vsub_eq_vsub_rev _ s.center, angle_neg_right, h1]
  linarith

Похожие утверждения