Defs

📁 Source: Mathlib/Logic/Small/Defs.lean

Statistics

Metric	Count
Definitions rec, equivShrink	2
Theorems ext, ext_iff, rec_equivShrink, equiv_small, mk', instNontrivialShrink, not_small_type, small_congr, small_iff, small_lift, small_map, small_max, small_plift, small_self, small_sigma, small_succ, small_type, small_ulift, small_zero	19
Total	21

Shrink

Definitions

Name	Category	Theorems
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	DFunLike.coe Equiv Shrink EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivShrink	—	—	EquivLike.toEmbeddingLike
ext_iff 📖	mathematical	—	DFunLike.coe Equiv Shrink EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivShrink	—	ext
rec_equivShrink 📖	mathematical	—	DFunLike.coe Equiv Shrink EquivLike.toFunLike Equiv.instEquivLike equivShrink	—	Equiv.symm_apply_apply

Small

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_small 📖	mathematical	—	Equiv	—	—
mk' 📖	mathematical	—	Small	—	—

(root)

Definitions

Name	Category	Theorems
equivShrink 📖	CompOp	60 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, CategoryTheory.ShrinkHoms.id_def, equivShrink_symm_div, equivShrink_symm_sub, Shrink.linearEquiv_symm_apply, CommRing.Pic.mul_eq_tensor, equivShrink_top, CategoryTheory.Subobject.wideCospan_map_term, equivShrink_symm_bot, CategoryTheory.Limits.Types.Small.productIso_inv_comp_π, CommRing.Pic.inv_eq_dual, equivShrink_symm_zero, CommRing.Pic.mk_eq_iff, CommRing.Pic.mk_eq_self, CommRing.Pic.mapAlgebra_apply, CommRing.Pic.ext_iff, CommRing.Pic.instFreeAsModuleOfNat, Shrink.ext_iff, equivShrink_symm_top, CategoryTheory.FunctorToTypes.shrink_map, CategoryTheory.CountableCategory.instLocallySmallObjAsType, equivShrink_div, CategoryTheory.Limits.Types.Small.productIso_inv_comp_π_apply, equivShrink_mul, Shrink.algEquiv_apply, CategoryTheory.Limits.Types.Small.limitCone_pt_ext_iff, CategoryTheory.Limits.Types.Small.limitCone_π_app, Shrink.toEquiv_homeomorph, CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small, CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift, AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality, equivShrink_lt_equivShrink, equivShrink_add, 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, equivShrink_inv, CategoryTheory.ShrinkHoms.comp_def, CategoryTheory.ShrinkHoms.inverse_map, equivShrink_smul, equivShrink_le_equivShrink, CategoryTheory.ShrinkHoms.functor_map, equivShrink_neg, equivShrink_symm_mul, equivShrink_symm_inv, equivShrink_symm_one, Shrink.linearEquiv_apply, equivShrink_symm_neg, equivShrink_symm_smul, equivShrink_bot, Shrink.algEquiv_symm_apply, equivShrink_sub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNontrivialShrink 📖	mathematical	—	Nontrivial Shrink	—	Equiv.nontrivial
not_small_type 📖	mathematical	—	Small	—	Function.cantor_injective Equiv.left_inv
small_congr 📖	mathematical	—	Small	—	small_map
small_iff 📖	mathematical	—	Small Equiv	—	—
small_lift 📖	mathematical	—	Small	—	Small.mk'
small_map 📖	mathematical	—	Small	—	Small.equiv_small Small.mk'
small_max 📖	mathematical	—	Small	—	small_lift small_self
small_plift 📖	mathematical	—	Small	—	small_map
small_self 📖	mathematical	—	Small	—	Small.mk'
small_sigma 📖	—	Small	—	—	Equiv.symm_apply_apply Shrink.congr_simp
small_succ 📖	mathematical	—	Small	—	small_lift small_self
small_type 📖	mathematical	—	Small	—	small_max
small_ulift 📖	mathematical	—	Small	—	small_map
small_zero 📖	mathematical	—	Small	—	small_max

---

← Back to Index