mapEquiv_symm_apply

Mathlib.Logic.Equiv.Functor

URI: https://scilib.ai/kg/mathlib#Bifunctor.mapEquiv_symm_apply

← MathLib Explorer

English

The inverse mapEquiv sends y to bimap h.symm h'.symm y.

Русский

Обратное mapEquiv отправляет y к bimap(h.symm,h'.symm) y.

LaTeX

$$$ (\\text{mapEquiv } F\; h\; h').\\mathrm{symm} y = \\text{bimap } h^{-1}\\, h'^{-1}\\, y $$$

Lean4

@[simp]
theorem mapEquiv_symm_apply (h : α ≃ β) (h' : α' ≃ β') (y : F β β') :
    (mapEquiv F h h' : F α α' ≃ F β β').symm y = bimap h.symm h'.symm y :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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