dist_pointReflection_fixed — Mathlib

English

For any x, y ∈ P, the distance from the reflection of y about x to x equals the distance between y and x: dist(pointReflection x y, x) = dist(y, x).

Русский

Для любых x, y ∈ P расстояние от отражённой точки y оx до x равно расстоянию между y и x: dist(pointReflection x y, x) = dist(y, x).

LaTeX

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

Lean4

@[simp]
theorem dist_pointReflection_fixed (x y : P) : dist (pointReflection 𝕜 x y) x = dist y x := by
  rw [← (pointReflection 𝕜 x).dist_map y x, pointReflection_self]

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