secondInter_eq_lineMap — Mathlib

English

SecondInter with p'−p corresponds to a line map with a linear fractional coefficient depending on p,p' and sphere center.

Русский

SecondInter для p'−p эквивалентно линейно-дробному отображению линии, зависящему от p,p' и центра сферы.

LaTeX

$$$s.secondInter(p,p' - p) = \\text{LineMap}_{p,p'}(...)$$$

Lean4

/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, the result of `secondInter` may be expressed using `lineMap`. -/
theorem secondInter_eq_lineMap (s : Sphere P) (p p' : P) :
    s.secondInter p (p' -ᵥ p) = AffineMap.lineMap p p' (-2 * ⟪p' -ᵥ p, p -ᵥ s.center⟫ / ⟪p' -ᵥ p, p' -ᵥ p⟫) :=
  rfl

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