# Instances and theorems for Small. #

In particular we prove small_of_injective and small_of_surjective.

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

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.

instance small_Pi {α : Type u_2} (β : αType u_1) [] [∀ (a : α), Small.{w, u_1} (β a)] :
Small.{w, max u_1 u_2} ((a : α) → β a)
Equations
• =
instance small_prod {α : Type u_1} {β : Type u_2} [] [] :
Equations
• =
instance small_sum {α : Type u_1} {β : Type u_2} [] [] :
Equations
• =
instance small_set {α : Type u_1} [] :
Equations
• =