self_comp_coe_symm — Mathlib

English

The composition e ∘ (e.toEquiv).symm equals id; i.e., the action of e followed by its inverse is identity.

Русский

Составление e ∘ (e.toEquiv).symm даёт тождество; действие e далее его обратного является тождеством.

LaTeX

$$$e \\circ (e:\\alpha \\simeq \\beta).\\mathrm{symm} = \\mathrm{id}$$$

Lean4

@[simp]
theorem _root_.EquivLike.self_comp_coe_symm {F} [EquivLike F α β] (e : F) : e ∘ (e : α ≃ β).symm = id :=
  (e : α ≃ β).self_comp_symm

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