whiskerLeft

Mathlib.CategoryTheory.Limits.VanKampen

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.Equifibered.whiskerLeft

← MathLib Explorer

English

If α is equifibered and H: K ⥤ J, then whiskerLeft H α is equifibered.

Русский

Если α равнолистовое и H: K ⥤ J, то whiskerLeft H α равно равнолистовым.

LaTeX

$$Equifibered α → (whiskerLeft H α) is Equifibered$$

Lean4

theorem whiskerLeft {K : Type*} [Category K] {F G : J ⥤ C} {α : F ⟶ G} (hα : Equifibered α) (H : K ⥤ J) :
    Equifibered (whiskerLeft H α) := fun _ _ f => hα (H.map f)

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

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

Разделы

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

Аффилиация

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