toEquiv_symm — Mathlib

English

For a coalgebra equivalence e : A ≃ₗc[R] B, the induced equivalence e.symm has the same underlying Equiv type and symmetry as the original, i.e., the symmetry of the linear equivalence part matches the inverse equivalence.

Русский

Для коалгебрального эквивалента e : A ≃ₗc[R] B сопряжённая симметрия e.symm имеет тот же базовый эквивалент и симметрию, что и исходный объект, т.е. симметрия линейного эквивалента совпадает с обратной эквивалентностью.

LaTeX

$$$ e^{\\mathrm{symm}}_{\\toEquiv} = e^{\\mathrm{toEquiv}}_{\\mathrm{symm}} $$$

Lean4

@[simp]
theorem toEquiv_symm : e.symm.toEquiv = e.toEquiv.symm :=
  rfl

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