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

source

ink

class Small (α : Type v) :

Prop

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

source

ink

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

Small α

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

source

ink

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

Type w

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

Equations

Shrink α = Classical.choose (_ : ∃ S, Nonempty (α ≃ S))

source

ink

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

α ≃ Shrink α

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

Equations

equivShrink α = Nonempty.some (_ : Nonempty (α ≃ Classical.choose (_ : ∃ S, Nonempty (α ≃ S))))

source

ink

instance small_self (α : Type v) :

Small α

Equations

small_self = small_self.proof_1

source

ink

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

Small α

source

ink

theorem small_lift (α : Type u) [hα : Small α] :

Small α

source

ink

instance small_max (α : Type v) :

Small α

Equations

small_max = small_max.proof_1

source

ink

instance small_ulift (α : Type u) [inst : Small α] :

Small (ULift α)

Equations

small_ulift = small_ulift.proof_1

source

ink

theorem small_type :

Small (Type u)

source

ink

theorem small_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

Small α ↔ Small β

source

ink

instance small_subtype (α : Type v) [inst : Small α] (P : α → Prop) :

Small { x // P x }

Equations

small_subtype = small_subtype.proof_1

source

ink

theorem small_of_injective {α : Type v} {β : Type w} [inst : Small β] {f : α → β} (hf : Function.Injective f) :

Small α

source

ink

theorem small_of_surjective {α : Type v} {β : Type w} [inst : Small α] {f : α → β} (hf : Function.Surjective f) :

Small β

source

ink

theorem small_subset {α : Type v} {s : Set α} {t : Set α} (hts : t ⊆ s) [inst : Small ↑s] :

Small ↑t

source

ink

instance small_subsingleton (α : Type v) [inst : Subsingleton α] :

Small α

Equations

small_subsingleton = small_subsingleton.proof_1

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

source

ink

instance small_Pi {α : Type u_1} (β : α → Type u_2) [inst : Small α] [inst : ∀ (a : α), Small (β a)] :

Small ((a : α) → β a)

Equations

@small_Pi = @small_Pi.proof_1

source

ink

instance small_sigma {α : Type u_1} (β : α → Type u_2) [inst : Small α] [inst : ∀ (a : α), Small (β a)] :

Small ((a : α) × β a)

Equations

@small_sigma = @small_sigma.proof_1

source

ink

instance small_prod {α : Type u_1} {β : Type u_2} [inst : Small α] [inst : Small β] :

Small (α × β)

Equations

@small_prod = @small_prod.proof_1

source

ink

instance small_sum {α : Type u_1} {β : Type u_2} [inst : Small α] [inst : Small β] :

Small (α ⊕ β)

Equations

@small_sum = @small_sum.proof_1

source

ink

instance small_set {α : Type u_1} [inst : Small α] :

Small (Set α)

Equations

@small_set = @small_set.proof_1

source

ink

instance small_range {α : Type v} {β : Type w} (f : α → β) [inst : Small α] :

Small ↑(Set.range f)

Equations

@small_range = @small_range.proof_1

source

ink

instance small_image {α : Type v} {β : Type w} (f : α → β) (S : Set α) [inst : Small ↑S] :

Small ↑(f '' S)

Equations

@small_image = @small_image.proof_1

source

ink

theorem not_small_type :

¬Small (Type (maxuv))