English
If the map x ↦ 2·x on G is injective, then pointReflection x y = y if and only if y = x (with the stated injectivity assumption).
Русский
При инъективности удвоения на G выполняется: pointReflection x y = y тогда и только тогда, когда y = x (при условии инъективности).
LaTeX
$$$$ \text{pointReflection } x y = y \iff y = x \quad \text{(under injectivity of }(2\cdot)\text{ on }G) $$$$
Lean4
/-- `x` is the only fixed point of `pointReflection x`. This lemma requires
`x + x = y + y ↔ x = y`. There is no typeclass to use here, so we add it as an explicit argument. -/
theorem pointReflection_fixed_iff_of_injective_two_nsmul {x y : P} (h : Injective (2 • · : G → G)) :
pointReflection x y = y ↔ y = x := by
rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero, ← two_nsmul,
← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
