MultiequalizerPullback

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/MultiequalizerPullback.lean

Statistics

Metric	Count
Definitions multicofork	1
Theorems isPushout, multicofork_π_eq_inl, multicofork_π_eq_inr	3
Total	4

CategoryTheory.Limits.Multicofork.IsColimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPushout 📖	mathematical	CategoryTheory.Limits.MultispanShape.R Set Set.instInsert CategoryTheory.Limits.MultispanShape.fst CategoryTheory.Limits.MultispanShape.L Unique.instInhabited Set.instSingletonSet CategoryTheory.Limits.MultispanShape.snd Set.univ	CategoryTheory.IsPushout CategoryTheory.Limits.MultispanIndex.left CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.MultispanIndex.fst CategoryTheory.Limits.MultispanIndex.snd CategoryTheory.Limits.Multicofork.π	—	CategoryTheory.Limits.Multicofork.condition isPushout.multicofork_π_eq_inl CategoryTheory.Limits.IsColimit.fac isPushout.multicofork_π_eq_inr hom_ext Eq.le Set.mem_univ

CategoryTheory.Limits.Multicofork.IsColimit.isPushout

Definitions

Name	Category	Theorems
multicofork 📖	CompOp	2 math math: multicofork_π_eq_inr, multicofork_π_eq_inl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multicofork_π_eq_inl 📖	mathematical	CategoryTheory.Limits.MultispanShape.R Set Set.instInsert CategoryTheory.Limits.MultispanShape.fst CategoryTheory.Limits.MultispanShape.L Unique.instInhabited Set.instSingletonSet CategoryTheory.Limits.MultispanShape.snd Set.univ	CategoryTheory.Limits.Multicofork.π multicofork CategoryTheory.Limits.PushoutCocone.inl CategoryTheory.Limits.MultispanIndex.left CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanIndex.fst CategoryTheory.Limits.MultispanIndex.snd	—	CategoryTheory.eqToHom_refl CategoryTheory.Category.id_comp
multicofork_π_eq_inr 📖	mathematical	CategoryTheory.Limits.MultispanShape.R Set Set.instInsert CategoryTheory.Limits.MultispanShape.fst CategoryTheory.Limits.MultispanShape.L Unique.instInhabited Set.instSingletonSet CategoryTheory.Limits.MultispanShape.snd Set.univ	CategoryTheory.Limits.Multicofork.π multicofork CategoryTheory.Limits.PushoutCocone.inr CategoryTheory.Limits.MultispanIndex.left CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanIndex.fst CategoryTheory.Limits.MultispanIndex.snd	—	CategoryTheory.eqToHom_refl CategoryTheory.Category.id_comp

---

← Back to Index