# Instances and theorems for `Small`. #

In particular we prove `small_of_injective` and `small_of_surjective`.

source
instance small_subtype (α : Type v) [Small.{w, v} α] (P : α → Prop) :
Small.{w, v} { x : α // P x }
source
theorem small_of_injective {α : Type v} {β : Type w} [Small.{u, w} β] {f : α → β} (hf : Function.Injective f) :
Small.{u, v} α
source
theorem small_of_surjective {α : Type v} {β : Type w} [Small.{u, v} α] {f : α → β} (hf : Function.Surjective f) :
Small.{u, w} β
source
@[instance 100]
instance small_subsingleton (α : Type v) [Subsingleton α] :
Small.{w, v} α
source
theorem small_of_injective_of_exists {α : Type v} {β : Type w} {γ : Type v'} [Small.{u, v} α] (f : α → γ) {g : β → γ} (hg : Function.Injective g) (h : ∀ (b : β), ∃ (a : α), f a = g b) :
Small.{u, w} β

This can be seen as a version of `small_of_surjective` in which the function `f` doesn't actually land in `β` but in some larger type `γ` related to `β` via an injective function `g`.

We don't define `Countable.toSmall` in this file, to keep imports to `Logic` to a minimum.

source
instance small_Pi {α : Type u_2} (β : α → Type u_1) [Small.{w, u_2} α] [∀ (a : α), Small.{w, u_1} (β a)] :
Small.{w, max u_1 u_2} ((a : α) → β a)
source
instance small_prod {α : Type u_1} {β : Type u_2} [Small.{w, u_1} α] [Small.{w, u_2} β] :
Small.{w, max u_2 u_1} (α × β)
source
instance small_sum {α : Type u_1} {β : Type u_2} [Small.{w, u_1} α] [Small.{w, u_2} β] :
Small.{w, max u_2 u_1} (α ⊕ β)
source
instance small_set {α : Type u_1} [Small.{w, u_1} α] :
Small.{w, u_1} (Set α)
source
instance small_quot {α : Type u} [Small.{v, u} α] (r : α → α → Prop) :
Small.{v, u} (Quot r)
source
instance small_quotient {α : Type u} [Small.{v, u} α] (s : Setoid α) :
Small.{v, u} (Quotient s)