eq_of_isTangentAt — Mathlib

English

If two points p and q both have tangents to the same affine subspace as to the sphere S, then p = q.

Русский

Если две точки p и q имеют касания одной и той же сферы S к подпространству as, то p = q.

LaTeX

$$$ s.IsTangentAt p as \\rightarrow s.IsTangentAt q as \\rightarrow p = q $$$

Lean4

theorem eq_of_isTangentAt {s : Sphere P} {p q : P} {as : AffineSubspace ℝ P} (hp : s.IsTangentAt p as)
    (hq : s.IsTangentAt q as) : p = q :=
  by
  have hqp := hp.inner_left_eq_zero_of_mem hq.mem_space
  have hpq := hq.inner_left_eq_zero_of_mem hp.mem_space
  rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero, ← hpq, ← sub_eq_zero, ← inner_sub_right,
    vsub_sub_vsub_cancel_right] at hqp
  simpa using hqp

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