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	—	CategoryTheory.Epi SSet SSet.largeCategory	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits SSet.hasColimits finite SSet.instFiniteSigmaObjOfFinite SSet.stdSimplex.instFiniteObjSimplexCategory CategoryTheory.isCardinalPresentable_of_isColimit' Cardinal.fact_isRegular_aleph0 CategoryTheory.Limits.Types.hasLimitsOfShape Opposite.small CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self hasCardinalLT_of_finite CategoryTheory.instFiniteArrowDiscrete le_refl instIsFinitelyPresentableObjSimplexCategoryStdSimplex SSet.range_eq_iSup_sigma_ι CategoryTheory.Limits.Types.hasColimitsOfSize CategoryTheory.Limits.colimit.ι_desc SSet.Subcomplex.range_eq_ofSimplex Equiv.apply_symm_apply
instIsFinitelyPresentable 📖	mathematical	—	CategoryTheory.IsFinitelyPresentable SSet SSet.largeCategory	—	exists_epi_from_isCardinalPresentable CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits SSet.hasLimits 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 UnivLE.small univLE_of_max UnivLE.self hasCardinalLT_of_finite CategoryTheory.Arrow.finite le_refl
instIsFinitelyPresentableObjSimplexCategoryStdSimplex 📖	mathematical	—	CategoryTheory.IsFinitelyPresentable SSet SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex	—	CategoryTheory.Presheaf.instIsCardinalPresentableFunctorOppositeTypeObjUliftYonedaOfHasColimitsOfSize CategoryTheory.Limits.Types.hasColimitsOfSize univLE_of_max UnivLE.self Cardinal.fact_isRegular_aleph0

---

← Back to Index