# Small types #

A type is w-small if there exists an equivalence to some S : Type w.

We provide a noncomputable model Shrink α : Type w, and equivShrink α : α ≃ Shrink α.

A subsingleton type is w-small for any w.

If α ≃ β, then Small.{w} α ↔ Small.{w} β.

See Mathlib.Logic.Small.Basic for further instances and theorems.

theorem small_iff (α : Type v) :
∃ (S : Type w), Nonempty (α S)
class Small (α : Type v) :

A type is Small.{w} if there exists an equivalence to some S : Type w.

• equiv_small : ∃ (S : Type w), Nonempty (α S)

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

Instances
theorem Small.equiv_small {α : Type v} [self : ] :
∃ (S : Type w), Nonempty (α S)

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

theorem Small.mk' {α : Type v} {S : Type w} (e : α S) :

Constructor for Small α from an explicit witness type and equivalence.

def Shrink (α : Type v) [] :

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

Equations
Instances For
noncomputable def equivShrink (α : Type v) [] :
α

The noncomputable equivalence between a w-small type and a model.

Equations
• = .some
Instances For
theorem Shrink.ext_iff {α : Type v} [] {x : } {y : } :
x = y (equivShrink α).symm x = (equivShrink α).symm y
theorem Shrink.ext {α : Type v} [] {x : } {y : } (w : (equivShrink α).symm x = (equivShrink α).symm y) :
x = y
noncomputable def Shrink.rec {α : Type u_1} [] {F : Sort v} (h : (X : α) → F ((equivShrink α) X)) (X : ) :
F X
Equations
Instances For
@[instance 101]
instance small_self (α : Type v) :
Equations
• =
theorem small_map {α : Type u_1} {β : Type u_2} [hβ : ] (e : α β) :
theorem small_lift (α : Type u) [hα : ] :
theorem small_max (α : Type v) :
instance small_zero (α : Type) :
Equations
• =
@[instance 100]
instance small_succ (α : Type v) :
Equations
• =
instance small_ulift (α : Type u) [] :
Equations
• =
theorem small_congr {α : Type u_1} {β : Type u_2} (e : α β) :
instance small_sigma {α : Type u_2} (β : αType u_1) [] [∀ (a : α), Small.{w, u_1} (β a)] :
Small.{w, max u_1 u_2} ((a : α) × β a)
Equations
• =