instHasPullbackFOfHasPullbacksPresieve₀_1

Mathlib.CategoryTheory.Sites.Hypercover.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1

← MathLib Explorer

English

Same as above; HasPullback f (E.f i) for E : PreZeroHypercover X and f : Y → X.

Русский

То же, HasPullback f (E.f i) при E : PreZeroHypercover X и f: Y → X.

LaTeX

$$HasPullback f (E.f i)$$

Lean4

instance {X Y : C} (E : PreZeroHypercover X) (f : Y ⟶ X) [E.presieve₀.HasPullbacks f] (i : E.I₀) :
    HasPullback f (E.f i) :=
  hasPullback_symmetry (E.f i) f

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

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

Разделы

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

Аффилиация

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