Instances and theorems for Small.

In particular we prove small_of_injective and small_of_surjective.

instance small_subtype (α : Type v) [Small.{w, v} α] (P : α → Prop) : Small.{w, v} { x : α // P x }

Equations

• (_ : Small.{w, v} { x : α // P x }) = (_ : Small.{w, v} { x : α // P x })

theorem small_of_injective {α : Type v} {β : Type w} [Small.{u, w} β] {f : α → β} (hf : Function.Injective f) : Small.{u, v} α

theorem small_of_surjective {α : Type v} {β : Type w} [Small.{u, v} α] {f : α → β} (hf : Function.Surjective f) : Small.{u, w} β

theorem small_subset {α : Type v} {s : Set α} {t : Set α} (hts : t ⊆ s) [Small.{u, v} ↑s] : Small.{u, v} ↑t

instance small_subsingleton (α : Type v) [Subsingleton α] : Small.{w, v} α

Equations

• (_ : Small.{w, v} α) = (_ : Small.{w, v} α)

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 small_of_fintype or small_of_countable in this file, to keep imports to Logic to a minimum.

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)

Equations

• (_ : Small.{w, max u_1 u_2} ((a : α) → β a)) = (_ : Small.{w, max u_1 u_2} ((a : α) → β a))

instance small_prod {α : Type u_1} {β : Type u_2} [Small.{w, u_1} α] [Small.{w, u_2} β] : Small.{w, max u_2 u_1} (α × β)

Equations

• (_ : Small.{w, max u_2 u_1} (α × β)) = (_ : Small.{w, max u_1 u_2} (α × β))

instance small_sum {α : Type u_1} {β : Type u_2} [Small.{w, u_1} α] [Small.{w, u_2} β] : Small.{w, max u_2 u_1} (α ⊕ β)

Equations

• (_ : Small.{w, max u_2 u_1} (α ⊕ β)) = (_ : Small.{w, max u_1 u_2} (α ⊕ β))

instance small_set {α : Type u_1} [Small.{w, u_1} α] : Small.{w, u_1} (Set α)

Equations

• (_ : Small.{w, u_1} (Set α)) = (_ : Small.{w, u_1} (Set α))

instance small_range {α : Type v} {β : Type w} (f : α → β) [Small.{u, v} α] : Small.{u, w} ↑(Set.range f)

Equations

• (_ : Small.{u, w} ↑(Set.range f)) = (_ : Small.{u, w} ↑(Set.range f))

instance small_image {α : Type v} {β : Type w} (f : α → β) (S : Set α) [Small.{u, v} ↑S] : Small.{u, w} ↑(f '' S)

Equations

• (_ : Small.{u, w} ↑(f '' S)) = (_ : Small.{u, w} ↑(f '' S))