English
For x,y in P, dist(pointReflection x y, y) equals twice the distance between x and y when considered via a suitable fixed point context.
Русский
Для x,y в P расстояние между pointReflection x y и y равно 2 dist(x,y) в подходящем контексте фиксации точки.
LaTeX
$$$\operatorname{dist}(\operatorname{pointReflection}_{\mathbb{k}}(x)(y), y) = 2 \cdot \operatorname{dist}(x,y)$$$
Lean4
/-- An affine subspace is isomorphic to its image under an injective affine map.
This is the affine version of `Submodule.equivMapOfInjective`.
-/
@[simps linear, simps! toFun]
noncomputable def equivMapOfInjective (E : AffineSubspace 𝕜 P₁) [Nonempty E] (φ : P₁ →ᵃ[𝕜] P₂)
(hφ : Function.Injective φ) : E ≃ᵃ[𝕜] E.map φ :=
{
Equiv.Set.image _ (E : Set P₁)
hφ with
linear :=
(E.direction.equivMapOfInjective φ.linear (φ.linear_injective_iff.mpr hφ)).trans
(LinearEquiv.ofEq _ _ (AffineSubspace.map_direction _ _).symm)
map_vadd' := fun p v => Subtype.ext <| φ.map_vadd p v }
