trans_apply — Mathlib

English

The action of the composite on an element a ∈ A is given by applying e1 first, then e2: (e1.trans e2) a = e2(e1(a)).

Русский

Действие составленного отображения на элемент a равно применению сначала e1, затем e2: (e1.trans e2) a = e2(e1(a)).

LaTeX

$$$(e_1 \mathrm{trans} e_2)\,a = e_2(e_1(a))$$$

Lean4

@[simp]
theorem trans_apply (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) (a : A) : (e₁.trans e₂) a = e₂ (e₁ a) :=
  rfl

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