WeaklyInitial

📁 Source: Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean

Statistics

Metric	Count
Definitions	0
Theorems hasInitial_of_weakly_initial_and_hasWideEqualizers, has_weakly_initial_of_weakly_initial_set_and_hasProducts	2
Total	2

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasInitial_of_weakly_initial_and_hasWideEqualizers 📖	mathematical	Limits.HasWideEqualizers Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	Limits.HasInitial	—	Limits.hasLimitOfHasLimitsOfShape Limits.hasEqualizers_of_hasWideEqualizers Category.assoc Limits.wideEqualizer.condition cancel_epi IsSplitEpi.epi IsSplitEpi.mk' cancel_mono_id Limits.wideEqualizer.ι_mono Category.comp_id Limits.equalizer.condition Limits.hasInitial_of_unique Unique.instSubsingleton
has_weakly_initial_of_weakly_initial_set_and_hasProducts 📖	—	Limits.HasProducts Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	—	—	Limits.hasLimitOfHasLimitsOfShape

---

← Back to Index