pointReflection — Mathlib

English

Define the point reflection in a fixed point x in an affine space as the composition of a sub-translation by x and a translation by x.

Русский

Определение точечного отражения в точке x как композиция вычитания по x и при этом прибавления x.

LaTeX

$$pointReflection(k,x) = (constVSub k x) .trans (vaddConst k x)$$

Lean4

/-- Point reflection in `x` as a permutation. -/
def pointReflection (x : P₁) : P₁ ≃ᵃ[k] P₁ :=
  (constVSub k x).trans (vaddConst k x)

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