secondInter_secondInter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Applying `secondInter` twice returns the original point. -/
@[simp]
theorem secondInter_secondInter (s : Sphere P) (p : P) (v : V) : s.secondInter (s.secondInter p v) v = p :=
  by
  by_cases hv : v = 0; · simp [hv]
  have hv' : ⟪v, v⟫ ≠ 0 := inner_self_ne_zero.2 hv
  simp only [Sphere.secondInter, vadd_vsub_assoc, vadd_vadd, inner_add_right, inner_smul_right, div_mul_cancel₀ _ hv']
  rw [← @vsub_eq_zero_iff_eq V, vadd_vsub, ← add_smul, ← add_div]
  convert zero_smul ℝ _
  convert zero_div (G₀ := ℝ) _
  ring

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