flip

Mathlib.CategoryTheory.Localization.Bifunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.Lifting₂.flip

Lean4

noncomputable instance flip : Lifting₂ L₂ L₁ W₂ W₁ F.flip F'.flip where
  iso := (flipFunctor _ _ _).mapIso (Lifting₂.iso L₁ L₂ W₁ W₂ F F')

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

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

Разделы

Аффилиация

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