pointReflection_fixed_iff_of_injective_two_nsmul

English

Under the injectivity of 2·, pointReflection x fixes y only when y = x.

Русский

При инъективности 2· точечное отражение фиксирует y только при y = x.

LaTeX

$$pointReflection k x y = y ↔ y = x$$

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 • · : V₁ → V₁)) :
    pointReflection k x y = y ↔ y = x :=
  Equiv.pointReflection_fixed_iff_of_injective_two_nsmul h

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