mathlib3 documentation

logic.small.basic

Small types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A type is w-small if there exists an equivalence to some S : Type w.

We provide a noncomputable model shrink α : Type w, and equiv_shrink α : α ≃ shrink α.

A subsingleton type is w-small for any w.

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

source
@[class]
structure small (α : Type v) :
Prop

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

Instances of this typeclass
source
theorem small.mk' {α : Type v} {S : Type w} (e : α ≃ S) :
small α

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

source
@[nolint]
def shrink (α : Type v) [small α] :
Type w

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

Equations
source
noncomputable def equiv_shrink (α : Type v) [small α] :
α ≃ shrink α

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

Equations
source
@[protected, instance]
def small_self (α : Type v) :
small α
source
theorem small_map {α : Type u_1} {β : Type u_2} [hβ : small β] (e : α ≃ β) :
small α
source
theorem small_lift (α : Type u) [hα : small α] :
small α
source
@[protected, instance]
def small_max (α : Type v) :
small α
source
@[protected, instance]
def small_ulift (α : Type u) [small α] :
small (ulift α)
source
theorem small_type  :
small (Type u)
source
theorem small_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
small α ↔ small β
source
@[protected, instance]
def small_subtype (α : Type v) [small α] (P : α → Prop) :
small {x // P x}
source
theorem small_of_injective {α : Type v} {β : Type w} [small β] {f : α → β} (hf : function.injective f) :
small α
source
theorem small_of_surjective {α : Type v} {β : Type w} [small α] {f : α → β} (hf : function.surjective f) :
small β
source
theorem small_subset {α : Type v} {s t : set α} (hts : t ⊆ s) [small ↥s] :
small ↥t
source
@[protected, instance]
def small_subsingleton (α : Type v) [subsingleton α] :
small α

We don't define small_of_fintype or small_of_countable in this file, to keep imports to logic to a minimum.

source
@[protected, instance]
def small_Pi {α : Type u_1} (β : α → Type u_2) [small α] [∀ (a : α), small (β a)] :
small (Π (a : α), β a)
source
@[protected, instance]
def small_sigma {α : Type u_1} (β : α → Type u_2) [small α] [∀ (a : α), small (β a)] :
small (Σ (a : α), β a)
source
@[protected, instance]
def small_prod {α : Type u_1} {β : Type u_2} [small α] [small β] :
small (α × β)
source
@[protected, instance]
def small_sum {α : Type u_1} {β : Type u_2} [small α] [small β] :
small (α ⊕ β)
source
@[protected, instance]
def small_set {α : Type u_1} [small α] :
small (set α)
source
@[protected, instance]
def small_range {α : Type v} {β : Type w} (f : α → β) [small α] :
small ↥(set.range f)
source
@[protected, instance]
def small_image {α : Type v} {β : Type w} (f : α → β) (S : set α) [small ↥S] :
small ↥(f '' S)
source
theorem not_small_type  :
¬small (Type (max u v))