pointReflection_involutive — Mathlib

English

Over a module where 2 is invertible, for every y, the map x ↦ pointReflection k x y is injective.

Русский

В модуле, где 2 обратимо, для каждого y отображение x ↦ pointReflection k x y инъективно.

LaTeX

$$[Invertible(2:k)] → ∀ y, Injective (x ↦ pointReflection k x y)$$

Lean4

theorem pointReflection_involutive (x : P₁) : Involutive (pointReflection k x : P₁ → P₁) :=
  Equiv.pointReflection_involutive x

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