secondInter_neg — Mathlib

English

SecondInter is invariant under negating the direction vector.

Русский

SecondInter не изменяется при замене вектора направления на его противоположный.

LaTeX

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

Lean4

/-- `secondInter` is unchanged by negating the vector. -/
@[simp]
theorem secondInter_neg (s : Sphere P) (p : P) (v : V) : s.secondInter p (-v) = s.secondInter p v := by
  rw [← neg_one_smul ℝ v, s.secondInter_smul p v (by simp : (-1 : ℝ) ≠ 0)]

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