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 equivShrink α : α ≃ Shrink α.

A subsingleton type is w-small for any w.

If α ≃ β, then Small.{w} α ↔ Small.{w} β.

theorem Small_iff (α : Type v) : Small.{w, v} α ↔ ∃ S, Nonempty (α ≃ S)

class Small (α : Type v) : Prop

• equiv_small : ∃ S, Nonempty (α ≃ S)

  If a type is Small.{w}, then there exists an equivalence with some S : Type w

A type is Small.{w} if there exists an equivalence to some S : Type w.

theorem Small.mk' {α : Type v} {S : Type w} (e : α ≃ S) : Small.{w, v} α

Constructor for Small α from an explicit witness type and equivalence.

def Shrink (α : Type v) [Small.{w, v} α] : Type w

An arbitrarily chosen model in Type w for a w-small type.

noncomputable def equivShrink (α : Type v) [Small.{w, v} α] : α ≃ Shrink α

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

theorem Shrink.ext {α : Type v} [Small.{w, v} α] {x : Shrink α} {y : Shrink α} (w : ↑(equivShrink α).symm x = ↑(equivShrink α).symm y) : x = y

noncomputable def Shrink.rec {α : Type u_1} [Small.{w, u_1} α] {F : Shrink α → Sort v} (h : (X : α) → F (↑(equivShrink α) X)) (X : Shrink α) : F X

instance small_self (α : Type v) : Small.{v, v} α

theorem small_map {α : Type u_1} {β : Type u_2} [hβ : Small.{w, u_2} β] (e : α ≃ β) : Small.{w, u_1} α

theorem small_lift (α : Type u) [hα : Small.{v, u} α] : Small.{max v w, u} α

instance small_max (α : Type v) : Small.{max w v, v} α

instance small_ulift (α : Type u) [Small.{v, u} α] : Small.{v, max w u} (ULift.{w, u} α)

theorem small_type : Small.{max (u + 1) v, u + 1} (Type u)

theorem small_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Small.{w, u_1} α ↔ Small.{w, u_2} β

instance small_subtype (α : Type v) [Small.{w, v} α] (P : α → Prop) : 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} α

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)

instance small_sigma {α : 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)

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

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

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

instance small_range {α : Type v} {β : Type w} (f : α → β) [Small.{u, v} α] : 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)

theorem not_small_type : ¬Small.{u, max (u + 1) (v + 1)} (Type (max u v))