dist_center_inversion — Mathlib

English

A collection of identities describing how inversion interacts with line maps and homotheties.

Русский

Сводка тождеств об взаимодействии инверсии с линейными отображениями и гомотетией.

LaTeX

$$$\text{(relations between inversion, lineMap, homothety)}$$$

Lean4

/-- Distance from the center of an inversion to the image of a point under the inversion. This
formula accidentally works for `x = c`. -/
theorem dist_center_inversion (c x : P) (R : ℝ) : dist c (inversion c R x) = R ^ 2 / dist c x := by
  rw [dist_comm c, dist_comm c, dist_inversion_center]

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