injective_pointReflection_left_of_injective_two_nsmul

English

Under the same injectivity condition, the left-translation by a fixed y is injective.

Русский

При тех же условиях инъективности, слева по фиксированной y перенос инъективен.

LaTeX

$$injective_pointReflection_left_of_injective_two_nsmul(h, y) : Injective (x ↦ pointReflection k x y)$$

Lean4

theorem injective_pointReflection_left_of_injective_two_nsmul (h : Injective (2 • · : V₁ → V₁)) (y : P₁) :
    Injective fun x : P₁ => pointReflection k x y :=
  Equiv.injective_pointReflection_left_of_injective_two_nsmul h y

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