injective_pointReflection_left_of_injective_two_nsmul

English

If 2·· on G is injective, then the map x ↦ pointReflection x is injective on P.

Русский

Если инъективно отображение x ↦ 2·x на G, то отображение x ↦ pointReflection x по P инъективно.

LaTeX

$$$$ \\text{Injective }(x \\mapsto \\text{pointReflection } x) \;\\text{ on } P $$$$

Lean4

theorem injective_pointReflection_left_of_injective_two_nsmul {G P : Type*} [AddCommGroup G] [AddTorsor G P]
    (h : Injective (2 • · : G → G)) (y : P) : Injective fun x : P => pointReflection x y :=
  fun x₁ x₂ (hy : pointReflection x₁ y = pointReflection x₂ y) => by
  rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub, vsub_sub_vsub_cancel_right, ←
    neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy

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