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

A subsingleton type is w-small for any w.

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

class Small (α : Type v) :
  • If a type is Small.{w}, then there exists an equivalence with some S : Type w

    equiv_small : S, Nonempty (α S)

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) [inst : Small α] :

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

    Equations
    noncomputable def equivShrink (α : Type v) [inst : Small α] :
    α Shrink α

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

    Equations
    theorem small_map {α : Type u_1} {β : Type u_2} [hβ : Small β] (e : α β) :
    theorem small_lift (α : Type u) [hα : Small α] :
    instance small_ulift (α : Type u) [inst : Small α] :
    Equations
    theorem small_congr {α : Type u_1} {β : Type u_2} (e : α β) :
    instance small_subtype (α : Type v) [inst : Small α] (P : αProp) :
    Small { x // P x }
    Equations
    theorem small_of_injective {α : Type v} {β : Type w} [inst : Small β] {f : αβ} (hf : Function.Injective f) :
    theorem small_of_surjective {α : Type v} {β : Type w} [inst : Small α] {f : αβ} (hf : Function.Surjective f) :
    theorem small_subset {α : Type v} {s : Set α} {t : Set α} (hts : t s) [inst : Small s] :
    Small t

    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_1} (β : αType u_2) [inst : Small α] [inst : ∀ (a : α), Small (β a)] :
    Small ((a : α) → β a)
    Equations
    instance small_sigma {α : Type u_1} (β : αType u_2) [inst : Small α] [inst : ∀ (a : α), Small (β a)] :
    Small ((a : α) × β a)
    Equations
    instance small_prod {α : Type u_1} {β : Type u_2} [inst : Small α] [inst : Small β] :
    Small (α × β)
    Equations
    instance small_sum {α : Type u_1} {β : Type u_2} [inst : Small α] [inst : Small β] :
    Small (α β)
    Equations
    instance small_set {α : Type u_1} [inst : Small α] :
    Small (Set α)
    Equations
    instance small_range {α : Type v} {β : Type w} (f : αβ) [inst : Small α] :
    Equations
    instance small_image {α : Type v} {β : Type w} (f : αβ) (S : Set α) [inst : Small S] :
    Small ↑(f '' S)
    Equations