trans_apply — Mathlib

English

The symmetric of the transitive composition is the composition of the symmetric maps in reverse order.

Русский

Симметрическая часть композиции транзитивности равна композиции симметричных отображений в обратном порядке.

LaTeX

$$$(e_1.trans e_2)^{-1} = e_2^{-1} \\trans e_1^{-1}$$$

Lean4

@[simp]
theorem trans_apply (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) (m : M) : (e₁.trans e₂) m = e₂ (e₁ m) :=
  rfl

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