toFun_inducedStructureEquiv

Mathlib.ModelTheory.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.toFun_inducedStructureEquiv

English

The underlying function of inducedStructureEquiv is exactly the given bijection e.

Русский

Базовая функция у inducedStructureEquiv равна данной биекции e.

LaTeX

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

Lean4

@[simp]
theorem toFun_inducedStructureEquiv (e : M ≃ N) : DFunLike.coe (@inducedStructureEquiv L M N _ e) = e :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru