Presentable

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/Presentable.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_epi_from_isCardinalPresentable, instIsFinitelyPresentable, instIsFinitelyPresentableObjSimplexCategoryStdSimplex	3
Total	3

SSet.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_epi_from_isCardinalPresentable 📖	mathematical	—	SSet SSet.Finite CategoryTheory.IsFinitelyPresentable CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Epi	—	CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.Types.hasColimit CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self SSet.instFiniteSigmaObjOfFinite finite SSet.stdSimplex.instFiniteObjSimplexCategory CategoryTheory.isCardinalPresentable_of_isColimit' Cardinal.fact_isRegular_aleph0 CategoryTheory.Limits.Types.hasLimitsOfShape Opposite.small hasCardinalLT_of_finite CategoryTheory.instFiniteArrowDiscrete le_refl instIsFinitelyPresentableObjSimplexCategoryStdSimplex SSet.range_eq_iSup_sigma_ι CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CategoryTheory.Limits.Types.hasColimitsOfSize CategoryTheory.Limits.colimit.ι_desc SSet.Subcomplex.range_eq_ofSimplex Equiv.apply_symm_apply
instIsFinitelyPresentable 📖	mathematical	—	CategoryTheory.IsFinitelyPresentable SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types	—	exists_epi_from_isCardinalPresentable CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self SSet.instFinitePullback Cardinal.fact_isRegular_aleph0 CategoryTheory.IsRegularEpiCategory.regularEpiOfEpi SSet.instIsRegularEpiCategory CategoryTheory.isCardinalPresentable_of_isColimit' CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.IsPullback.of_hasPullback CategoryTheory.instEffectiveEpiOfIsRegularEpi CategoryTheory.Limits.Types.hasLimitsOfShape Opposite.small hasCardinalLT_of_finite CategoryTheory.Arrow.finite le_refl
instIsFinitelyPresentableObjSimplexCategoryStdSimplex 📖	mathematical	—	CategoryTheory.IsFinitelyPresentable SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex	—	—

---

← Back to Index