vadd_right_injective — Mathlib

English

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

Русский

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

LaTeX

$$$$ \text{Injective }(x \mapsto \text{pointReflection } x) $$$$

Lean4

/-- Adding a group element to the point `p` is an injective
function. -/
theorem vadd_right_injective (p : P) : Function.Injective ((· +ᵥ p) : G → P) := fun _ _ => vadd_right_cancel p

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