logic.small

# 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 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 α] :
Type w

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  :
small (Type u)
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))
@[protected, instance]
def small_vector {α : Type v} {n : } [small α] :
small (vector α n)
@[protected, instance]
def small_list {α : Type v} [small α] :
small (list α)