pointReflection_fixed_iff — Mathlib

English

In the real case, dist(pointReflection 𝕽 x y, y) = 2 · dist(x, y).

Русский

В вещественном случае dist(pointReflection ℝ x y, y) = 2 · dist(x, y).

LaTeX

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

Lean4

theorem pointReflection_fixed_iff [Invertible (2 : 𝕜)] {x y : P} : pointReflection 𝕜 x y = y ↔ y = x :=
  AffineEquiv.pointReflection_fixed_iff_of_module 𝕜

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