English
If e1: α ≃ β and e2: β ≃ γ, then the composition e2 ∘ e1 is an equivalence α ≃ γ with inverse e1^{-1} ∘ e2^{-1}.
Русский
Если e1: α ≃ β и e2: β ≃ γ, то композиция e2 ∘ e1 образует эквивалентность α ≃ γ с обратной последовательностью e1^{-1} ∘ e2^{-1}.
LaTeX
$$$\forall e_1:\alpha \simeq \beta,\ e_2:\beta \simeq \gamma,\ (e_2 \circ e_1) : \alpha \simeq \gamma \\ (e_2 \circ e_1)^{-1} = e_1^{-1} \circ e_2^{-1}$$$
Lean4
/-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`. -/
@[trans]
protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm, e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
