secondInter_mem — Mathlib

English

For a sphere and a tangent from a point p to t, the square of the tangent length equals the product of the secant segment lengths: dist(p,t)^2 = dist(p,a) dist(p,b) for appropriate a,b on the sphere.

Русский

Для сферы и касательной из точки p к точке t квадрат длины касательной равен произведению длин секантных отрезков: dist(p,t)^2 = dist(p,a) dist(p,b).

LaTeX

$$$\\operatorname{dist}(p,t)^2 = \\operatorname{dist}(p,a) \\cdot \\operatorname{dist}(p,b)$ under cospherical configuration$$

Lean4

/-- The point given by `secondInter` lies on the sphere. -/
@[simp]
theorem secondInter_mem {s : Sphere P} {p : P} (v : V) : s.secondInter p v ∈ s ↔ p ∈ s := by
  simp_rw [mem_sphere, Sphere.secondInter_dist]

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