dist_pointReflection_self — Mathlib

English

For any x, y ∈ P, dist(pointReflection x y, y) = ||2|| · dist(x, y). If the base field is 𝕜 with a norm, this equals 2 · dist(x, y).

Русский

Для любых x, y ∈ P расстояние между отражением x относительно y и y равно 2·dist(x, y).

LaTeX

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

Lean4

theorem dist_pointReflection_self (x y : P) : dist (pointReflection 𝕜 x y) y = ‖(2 : 𝕜)‖ * dist x y := by
  rw [dist_pointReflection_self', two_nsmul, ← two_smul 𝕜, norm_smul, ← dist_eq_norm_vsub V]

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