IsTangentAt_iff_angle_eq_pi_div_two

English

Through a point p on sphere s, the line through p and q is tangent to s if and only if ∠ q p s.center = π/2.

Русский

Через точку p на сфере s прямая pq касается сферы тогда и только тогда, когда ∠ q p s.center = π/2.

LaTeX

$$$s.IsTangentAt(p, line(p,q)) \\iff \\angle q p s.center = \\dfrac{\\pi}{2}$$$

Lean4

/-- A line through `p` is tangent to the sphere at `p` if and only if the angle between the line and
the radius at `p` equals `π / 2`. -/
theorem IsTangentAt_iff_angle_eq_pi_div_two {s : Sphere P} {p q : P} (hp : p ∈ s) :
    s.IsTangentAt p line[ℝ, p, q] ↔ ∠ q p s.center = π / 2 := by
  exact
    ⟨fun h ↦ IsTangentAt.angle_eq_pi_div_two h (right_mem_affineSpan_pair ℝ p q), fun h ↦
      IsTangentAt_of_angle_eq_pi_div_two h hp⟩

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