secondInter_dist — Mathlib

English

The second intersection point lies on the sphere exactly when the original point lies on the sphere.

Русский

Вторая точка пересечения лежит на сфере тогда и только тогда, когда исходная точка лежит на сфере.

LaTeX

$$$(s.secondInter p v) \\in s \\iff p \\in s$$$

Lean4

/-- The distance between `secondInter` and the center equals the distance between the original
point and the center. -/
@[simp]
theorem secondInter_dist (s : Sphere P) (p : P) (v : V) : dist (s.secondInter p v) s.center = dist p s.center :=
  by
  rw [Sphere.secondInter]
  by_cases hv : v = 0; · simp [hv]
  rw [dist_smul_vadd_eq_dist _ _ hv]
  exact Or.inr rfl

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