symm_trans_apply — Mathlib

English

The symmetry of a transitive composition reduces to the symmetric of each factor in reverse order.

Русский

Симметрия транспитивной композиции сводится к симметрии каждого множителя в обратном порядке.

LaTeX

$$$\\bigl(e_{12} \\text{.trans} e_{23}\\bigr)^{\\mathrm{symm}} = e_{23}^{\\mathrm{symm}} \\text{.trans} e_{12}^{\\mathrm{symm}}$$$

Lean4

theorem symm_trans_apply (c : M₃) : (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃).symm c = e₁₂.symm (e₂₃.symm c) :=
  rfl

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