# Documentation

Mathlib.Logic.Small.Basic

# 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) :
S, Nonempty (α S)
class Small (α : Type v) :
• 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.

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

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

def Shrink (α : Type v) [] :

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

Instances For
noncomputable def equivShrink (α : Type v) [] :
α

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

Instances For
theorem Shrink.ext {α : Type v} [] {x : } {y : } (w : ().symm x = ().symm y) :
x = y
noncomputable def Shrink.rec {α : Type u_1} [] {F : Sort v} (h : (X : α) → F (↑() X)) (X : ) :
F X
Instances For
instance small_self (α : Type v) :
theorem small_map {α : Type u_1} {β : Type u_2} [hβ : ] (e : α β) :
theorem small_lift (α : Type u) [hα : ] :
instance small_max (α : Type v) :
instance small_ulift (α : Type u) [] :
theorem small_congr {α : Type u_1} {β : Type u_2} (e : α β) :
instance small_subtype (α : Type v) [] (P : αProp) :
Small.{w, v} { x // P x }
theorem small_of_injective {α : Type v} {β : Type w} [] {f : αβ} (hf : ) :
theorem small_of_surjective {α : Type v} {β : Type w} [] {f : αβ} (hf : ) :
theorem small_subset {α : Type v} {s : Set α} {t : Set α} (hts : t s) [] :
instance small_subsingleton (α : Type v) [] :
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 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) [] [∀ (a : α), Small.{w, u_1} (β a)] :
Small.{w, max u_1 u_2} ((a : α) → β a)
instance small_sigma {α : Type u_2} (β : αType u_1) [] [∀ (a : α), Small.{w, u_1} (β a)] :
Small.{w, max u_1 u_2} ((a : α) × β a)
instance small_prod {α : Type u_1} {β : Type u_2} [] [] :
instance small_sum {α : Type u_1} {β : Type u_2} [] [] :
instance small_set {α : Type u_1} [] :
instance small_range {α : Type v} {β : Type w} (f : αβ) [] :
instance small_image {α : Type v} {β : Type w} (f : αβ) (S : Set α) [] :
Small.{u, w} ↑(f '' S)