Mathlib Map

Theorems · Definition · logic and foundations

Shrink

(α : Type v) → [Small.{w, v} α] → Type w

An arbitrarily chosen model in Type w for a w-small type.

Defined in
Mathlib.Logic.Small.Defs
Cited by
132 results in Mathlib
Foundations
Depth 8 from the axioms, rests on 11 definitions · uses Classical.choice
Assumes
Small
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

equivShrink · cited by 118equivShrinkCommRing.Pic · cited by 37CommRing.PicModule.Flat.rTensor_preserves_injective_linearMap · cited by 24Flat.rTensor_preserves_in…CategoryTheory.Localization.SmallHom · cited by 24Localization.SmallHomShrink.linearEquiv · cited by 19Shrink.linearEquivCategoryTheory.Shrink.equivalence · cited by 18Shrink.equivalenceZFSet.card · cited by 16ZFSet.cardModuleCat.localizedModule · cited by 16ModuleCat.localizedModuleCategoryTheory.FunctorToTypes.shrink · cited by 9FunctorToTypes.shrinkShrink.mulEquiv · cited by 8Shrink.mulEquivGrpCat.shrinkFunctor · cited by 6GrpCat.shrinkFunctorZFSet.range · cited by 6ZFSet.rangeorderIsoShrink · cited by 6orderIsoShrinkCategoryTheory.Limits.Types.Small.limitCone · cited by 6Small.limitConeCategoryTheory.Limits.Types.Small.productIso · cited by 6Small.productIsoSmall · cited by 369SmallSmall.equiv_small · cited by 4Small.equiv_smallShrinkCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by170

Results whose statement or proof uses this declaration.