Mathlib Map

Theorems · Theorem · logic and foundations

Small.equiv_small

∀ {α : Type v} [self : Small.{w, v} α], ∃ S, Nonempty (α ≃ S)

If a type is Small.{w}, then there exists an equivalence with some S : Type w

Defined in
Mathlib.Logic.Small.Defs
Cited by
4 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Small
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Shrink · cited by 132Shrinksmall_map · cited by 3small_mapAlgebraicGeometry.IsAffineOpen.iSup_of_disjoint · cited by 2IsAffineOpen.iSup_of_disj…Small.trans_univLE · cited by 1Small.trans_univLEAlgebraicGeometry.isOpenImmersion_sigmaDesc · cited by 1AlgebraicGeometry.isOpenI…Equiv · cited by 8337EquivSmall · cited by 369SmallSmall.equiv_smallCITED BYCITES

Cites2

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

  • Equivstatement · cited by 8,337
  • Smallstatement and proof · cited by 369

Cited by5

Results whose statement or proof uses this declaration.