reflection_reflectionPerm — Mathlib

English

Let i, j ∈ ι. Then the reflection at i of the permutation reflectionPerm(j, i) equals the product of reflections: reflection(P.reflectionPerm(j, i)) = reflection(j) ∘ reflection(i) ∘ reflection(j).

Русский

Пусть i, j ∈ ι. Тогда отражение в i от отражения reflectionPerm(j, i) равно композиции отражений: reflection(P.reflectionPerm(j, i)) = reflection(j) ∘ reflection(i) ∘ reflection(j).

LaTeX

$$$ P.reflection(P.reflectionPerm(j,i)) = P.reflection(j) \circ P.reflection(i) \circ P.reflection(j) $$$

Lean4

theorem reflection_reflectionPerm {i j : ι} :
    P.reflection (P.reflectionPerm j i) = P.reflection j * P.reflection i * P.reflection j := by ext x;
  simp [reflection_apply, coreflection_apply]; module

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