pointReflection_apply_eq_equivPointReflection_apply

English

The action of pointReflection on a point x coincides with the standard Equiv.pointReflection action on x.

Русский

Действие точечного отражения на точке x совпадает с обычным действием Equiv.pointReflection на x.

LaTeX

$$pointReflection(k,x) y = Equiv.pointReflection x y$$

Lean4

@[simp]
theorem pointReflection_apply_eq_equivPointReflection_apply (x y : P₁) :
    pointReflection k x y = Equiv.pointReflection x y :=
  rfl

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