map₂Iso_eqToIso

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PrelaxFunctor.map₂Iso_eqToIso

English

Equality under eqToIso is preserved by the functor map₂Iso.

Русский

Эквивалентность подeqToIso сохраняется функторным отображением map₂Iso.

LaTeX

$$$F.map₂Iso(\\mathrm{eqToIso}(hfg)) = \\mathrm{eqToIso}(hfg')$$$

Lean4

theorem map₂Iso_eqToIso {x y : B} (f g : x ⟶ y) (hfg : f = g) : F.map₂Iso (eqToIso hfg) = eqToIso (by rw [← hfg]) :=
  by
  subst hfg
  simp

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

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

Разделы

Аффилиация

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