liftingLift₂

Mathlib.CategoryTheory.Localization.Bifunctor

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

Lean4

noncomputable instance liftingLift₂ (X₁ : C₁) : Lifting L₂ W₂ (F.obj X₁) ((lift₂ F hF L₁ L₂).obj (L₁.obj X₁)) :=
  Lifting₂.fst _ _ W₁ _ _ _ _

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

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

Разделы

Аффилиация

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