sbtw_secondInter — Mathlib

English

Applying secondInter twice along the same vector returns the original point.

Русский

Повторное применение secondInter вдоль того же вектора возвращает исходную точку.

LaTeX

$$$s.secondInter(s.secondInter(p,v),v) = p$$$

Lean4

/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, and the second point is inside the sphere, the second point is strictly between
the first point and the result of `secondInter`. -/
theorem sbtw_secondInter {s : Sphere P} {p p' : P} (hp : p ∈ s) (hp' : dist p' s.center < s.radius) :
    Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p)) :=
  by
  refine ⟨Sphere.wbtw_secondInter hp hp'.le, ?_, ?_⟩
  · rintro rfl
    rw [mem_sphere] at hp
    simp [hp] at hp'
  · rintro h
    rw [h, mem_sphere.1 ((Sphere.secondInter_mem _).2 hp)] at hp'
    exact lt_irrefl _ hp'

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