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