ofTwoArrows

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sieve.ofTwoArrows

Lean4

/-- The sieve generated by two morphisms. -/
abbrev ofTwoArrows {U V X : C} (i : U ⟶ X) (j : V ⟶ X) : Sieve X :=
  Sieve.ofArrows (Y := pairFunction U V) (fun k ↦ WalkingPair.casesOn k i j)

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

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

Разделы

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

Аффилиация

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