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} β.

See Mathlib/Logic/Small/Basic.lean for further instances and theorems.

class Small (α : Type v) : Prop

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

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

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

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

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.

Equations

• Shrink.{?u.2, ?u.1} α = Classical.choose ⋯

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

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

Equations

• equivShrink α = ⋯.some

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

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

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

Equations

• Shrink.rec h X = ⋯ ▸ h ((equivShrink α).symm X)

@[simp]

theorem Shrink.rec_equivShrink {α : Type u_1} [Small.{w, u_1} α] {F : Shrink.{w, u_1} α → Sort v} {f : (a : α) → F ((equivShrink α) a)} (a : α) : Shrink.rec f ((equivShrink α) a) = f a

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} α

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

Due to https://github.com/leanprover/lean4/issues/2297, this is useless as an instance.

See however Logic.UnivLE, whose API is able to indirectly provide this instance.

instance small_zero (α : Type) : Small.{w, 0} α

@[instance 100]

instance small_succ (α : Type v) : Small.{v + 1, v} α

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

instance small_plift (α : Type u) [Small.{v, u} α] : Small.{v, u + 1} (PLift α)

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

instance instNontrivialShrink {α : Type u} [Small.{v, u} α] [Nontrivial α] : Nontrivial (Shrink.{v, u} α)

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

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)

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