toFun_inducedStructureEquiv_Symm — Mathlib

English

The underlying function of the symmetric inducedStructureEquiv is the inverse bijection e.symm.

Русский

Базовая функция симметричной inducedStructureEquiv равна обратной биекции e.symm.

LaTeX

$$$\mathrm{DFunLike}.coeff(\operatorname{inducedStructureEquiv}(e)^{\mathrm{symm}}) = e^{\mathrm{symm}}$$$

Lean4

@[simp]
theorem toFun_inducedStructureEquiv_Symm (e : M ≃ N) :
    (by letI : L.Structure N := inducedStructure e
        exact DFunLike.coe (@inducedStructureEquiv L M N _ e).symm) = (e.symm : N → M) :=
  rfl

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