# mathlib3documentation

logic.small.basic

# Small types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

We provide a noncomputable model shrink α : Type w, and equiv_shrink α : α ≃ shrink α.

A subsingleton type is w-small for any w.

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

@[class]
structure small (α : Type v) :
Prop

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

Instances of this typeclass
theorem small.mk' {α : Type v} {S : Type w} (e : α S) :

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

@[nolint]
def shrink (α : Type v) [small α] :

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

Equations
noncomputable def equiv_shrink (α : Type v) [small α] :
α

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

Equations
@[protected, instance]
def small_self (α : Type v) :
theorem small_map {α : Type u_1} {β : Type u_2} [hβ : small β] (e : α β) :
theorem small_lift (α : Type u) [hα : small α] :
@[protected, instance]
def small_max (α : Type v) :
@[protected, instance]
def small_ulift (α : Type u) [small α] :
theorem small_type  :
theorem small_congr {α : Type u_1} {β : Type u_2} (e : α β) :
@[protected, instance]
def small_subtype (α : Type v) [small α] (P : α Prop) :
small {x // P x}
theorem small_of_injective {α : Type v} {β : Type w} [small β] {f : α β} (hf : function.injective f) :
theorem small_of_surjective {α : Type v} {β : Type w} [small α] {f : α β} (hf : function.surjective f) :
theorem small_subset {α : Type v} {s t : set α} (hts : t s) [small s] :
@[protected, instance]
def small_subsingleton (α : Type v) [subsingleton α] :

We don't define small_of_fintype or small_of_countable in this file, to keep imports to logic to a minimum.

@[protected, instance]
def small_Pi {α : Type u_1} (β : α Type u_2) [small α] [ (a : α), small (β a)] :
small (Π (a : α), β a)
@[protected, instance]
def small_sigma {α : Type u_1} (β : α Type u_2) [small α] [ (a : α), small (β a)] :
small (Σ (a : α), β a)
@[protected, instance]
def small_prod {α : Type u_1} {β : Type u_2} [small α] [small β] :
small × β)
@[protected, instance]
def small_sum {α : Type u_1} {β : Type u_2} [small α] [small β] :
small β)
@[protected, instance]
def small_set {α : Type u_1} [small α] :
small (set α)
@[protected, instance]
def small_range {α : Type v} {β : Type w} (f : α β) [small α] :
@[protected, instance]
def small_image {α : Type v} {β : Type w} (f : α β) (S : set α) [small S] :
small (f '' S)
theorem not_small_type  :
¬small (Type (max u v))