mathlib documentation

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
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
def equiv_shrink (α : Type v) [small α] :
α shrink α

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

Equations
@[instance]
def small_self (α : Type v) :
@[instance]
def small_max (α : Type v) :
@[instance]
def small_ulift (α : Type v) :
theorem small_type  :
small (Type u)
theorem small_congr {α : Type u_1} {β : Type u_2} (e : α β) :
@[instance]
def small_subtype (α : Type v) [small α] (P : α → Prop) :
small {x // P x}
@[instance]
def small_of_fintype (α : Type v) [fintype α] :
theorem small_of_injective {α : Type u_1} {β : Type u_2} [small β] (f : α → β) (hf : function.injective f) :
@[instance]
def small_of_encodable (α : Type v) [encodable α] :
@[instance]
def small_Pi {α : Type u_1} (β : α → Type u_2) [small α] [∀ (a : α), small (β a)] :
small (Π (a : α), β a)
@[instance]
def small_sigma {α : Type u_1} (β : α → Type u_2) [small α] [∀ (a : α), small (β a)] :
small (Σ (a : α), β a)
@[instance]
def small_prod {α : Type u_1} {β : Type u_2} [small α] [small β] :
small × β)
@[instance]
def small_sum {α : Type u_1} {β : Type u_2} [small α] [small β] :
small β)
@[instance]
def small_set {α : Type u_1} [small α] :
small (set α)
theorem not_small_type  :
¬small (Type (max u v))