pi

Mathlib.CategoryTheory.MorphismProperty.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.pi

Lean4

/-- If `W j` are morphism properties on categories `C j` for all `j`, this is the
induced morphism property on the category `∀ j, C j`. -/
def pi {J : Type w} {C : J → Type u} [∀ j, Category.{v} (C j)] (W : ∀ j, MorphismProperty (C j)) :
    MorphismProperty (∀ j, C j) := fun _ _ f => ∀ j, (W j) (f j)

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

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

Разделы

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

Аффилиация

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