secondInter_zero — Mathlib

English

The secondInter point equals the evaluation of a line map with a certain linear fractional expression on p and p'.

Русский

Вторая точка пересечения равна значения линейного отображения линии, применённого к p и p'.

LaTeX

$$$s.secondInter(p,p' - p) = \\text{LineMap}_{p,p'}\\left(-2 \\frac{\\langle p' - p, p - s.center\\rangle}{\\langle p' - p, p' - p\\rangle}\\right)$$$

Lean4

/-- If the vector is zero, `secondInter` gives the original point. -/
@[simp]
theorem secondInter_zero (s : Sphere P) (p : P) : s.secondInter p (0 : V) = p := by simp [Sphere.secondInter]

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