Shrink

📁 Source: Mathlib/Topology/Instances/Shrink.lean

Statistics

Metric	Count
Definitions Shrink, homeomorph, instTopologicalSpace	3
Theorems toEquiv_homeomorph	1
Total	4

Shrink

Definitions

Name	Category	Theorems
homeomorph 📖	CompOp	1 math math: toEquiv_homeomorph
instTopologicalSpace 📖	CompOp	3 math math: toEquiv_homeomorph, continuousLinearEquiv_symm_apply, continuousLinearEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toEquiv_homeomorph 📖	mathematical	—	Homeomorph.toEquiv Shrink instTopologicalSpace homeomorph Equiv.symm Equiv.topologicalSpace equivShrink Equiv.homeomorph	—	—

(root)

Definitions

Name	Category	Theorems
Shrink 📖	CompOp	87 math math: CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval, CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply, CategoryTheory.CountableCategory.instObjAsType, CategoryTheory.FunctorToTypes.shrinkMap_app, Shrink.instIsRightCancelAdd, CategoryTheory.ShrinkHoms.id_def, equivShrink_symm_div, instNontrivialShrink, equivShrink_symm_sub, Shrink.instIsRightCancelMul, Shrink.linearEquiv_symm_apply, CategoryTheory.Shrink.instLocallySmallShrink, CommRing.Pic.mul_eq_tensor, equivShrink_top, CategoryTheory.Subobject.wideCospan_map_term, AddCommGrpCat.Colimits.colimitCocone_ι_app, equivShrink_symm_bot, CategoryTheory.Limits.Types.Small.productIso_inv_comp_π, Cardinal.lift_mk_shrink', CommRing.Pic.inv_eq_dual, equivShrink_symm_zero, CommRing.Pic.mk_eq_iff, CommRing.Pic.mk_eq_self, CategoryTheory.Limits.Types.Small.limitCone_pt, Module.Free.Module.free_shrink, CommRing.Pic.mapAlgebra_apply, CommRing.Pic.ext_iff, Shrink.instIsLeftCancelAdd, CommRing.Pic.instFreeAsModuleOfNat, AddCommGrpCat.Colimits.colimitCocone_pt, Shrink.ext_iff, Cardinal.lift_mk_shrink'', equivShrink_symm_top, CategoryTheory.FunctorToTypes.shrink_map, CategoryTheory.CountableCategory.instLocallySmallObjAsType, equivShrink_div, CategoryTheory.Limits.Types.Small.productIso_inv_comp_π_apply, Cardinal.lift_mk_shrink, equivShrink_mul, AddCommGrpCat.Colimits.Quot.desc_colimitCocone, Shrink.algEquiv_apply, instWellFoundedLTShrink, CategoryTheory.Limits.Types.Small.limitCone_pt_ext_iff, CategoryTheory.Limits.Types.Small.limitCone_π_app, Shrink.toEquiv_homeomorph, Shrink.instIsDomain, CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small, CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift, Fintype.card_shrink, AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality, equivShrink_lt_equivShrink, equivShrink_add, Module.Flat.shrink, CategoryTheory.CountableCategory.instCountableHomObjAsType, Shrink.continuousLinearEquiv_symm_apply, equivShrink_symm_add, Shrink.rec_equivShrink, orderIsoShrink_apply, Shrink.continuousLinearEquiv_apply, orderIsoShrink_symm_apply, CategoryTheory.Subobject.leInfCone_π_app_none, Shrink.instIsCancelAdd, equivShrink_inv, CategoryTheory.ShrinkHoms.comp_def, CategoryTheory.ShrinkHoms.inverse_map, Shrink.instIsCancelMul, equivShrink_smul, equivShrink_le_equivShrink, CategoryTheory.FunctorToTypes.shrink_obj, CategoryTheory.ShrinkHoms.functor_map, instWellFoundedGTShrink, Shrink.instIsLeftCancelMul, equivShrink_neg, Shrink.instFinite, CategoryTheory.hasCardinalLT_arrow_shrink_iff, equivShrink_symm_mul, instFreeCarrierX₂ModuleCatProjectiveShortComplex, equivShrink_symm_inv, Module.Finite.Module.finite_shrink, equivShrink_symm_one, Shrink.linearEquiv_apply, equivShrink_symm_neg, equivShrink_symm_smul, equivShrink_bot, Shrink.algEquiv_symm_apply, ModuleCat.isSeparator, equivShrink_sub

---

← Back to Index