mapEquiv_apply

Mathlib.Logic.Equiv.Functor

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

English

The mapEquiv for a bifunctor acts on x by bimap h h' on the component.

Русский

mapEquiv для бифункторa действует на x через bimap h h'.

LaTeX

$$$ (\\text{mapEquiv } F\; h\; h')\\, x = \\text{bimap } h\\, h'\\, x $$$

Lean4

@[simp]
theorem mapEquiv_apply (h : α ≃ β) (h' : α' ≃ β') (x : F α α') : (mapEquiv F h h' : F α α' ≃ F β β') x = bimap h h' x :=
  rfl

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

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

Разделы

Аффилиация

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