dist_sq_eq_of_mem — Mathlib

English

If s.IsTangentAt p to as and q ∈ as, then dist(q, center)^2 = radius^2 + dist(q, p)^2.

Русский

Если s IsTangentAt p к as и q ∈ as, тогда dist(q, центр)^2 = radius^2 + dist(q, p)^2.

LaTeX

$$$ (\\operatorname{dist} q \\; s.center)^2 = s.radius^2 + (\\operatorname{dist} q p)^2 $$$

Lean4

theorem dist_sq_eq_of_mem {s : Sphere P} {p q : P} {as : AffineSubspace ℝ P} (h : s.IsTangentAt p as) (hq : q ∈ as) :
    (dist q s.center) ^ 2 = s.radius ^ 2 + (dist q p) ^ 2 :=
  by
  rw [← h.mem_sphere]
  simp_rw [dist_eq_norm_vsub, pow_two]
  rw [← vsub_add_vsub_cancel q p s.center]
  conv_rhs => rw [add_comm]
  rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
  exact h.inner_left_eq_zero_of_mem hq

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