dist_pointReflection_self' — Mathlib

English

For x, y ∈ P, the distance between y and the reflection of x about y equals twice the distance between x and y: dist(pointReflection x y, y) = ||2 • (x −ᵥ y)||.

Русский

Для x, y ∈ P расстояние между y и отражением x относительно y равно дважды расстоянию между x и y: dist(pointReflection x y, y) = ||2 • (x −ᵥ y)||.

LaTeX

$$$\operatorname{dist}(\operatorname{pointReflection}_{\mathbb{k}}(x)(y), y) = \|2 \cdot (x -_v y)\|$$$

Lean4

theorem dist_pointReflection_self' (x y : P) : dist (pointReflection 𝕜 x y) y = ‖2 • (x -ᵥ y)‖ := by
  rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, two_nsmul]

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