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} β
.
The noncomputable equivalence between a w
-small type and a model.
Equations
- equivShrink α = Nonempty.some (_ : Nonempty (α ≃ Classical.choose (_ : ∃ S, Nonempty (α ≃ S))))
Equations
Equations
theorem
small_of_injective
{α : Type v}
{β : Type w}
[inst : Small β]
{f : α → β}
(hf : Function.Injective f)
:
Small α
theorem
small_of_surjective
{α : Type v}
{β : Type w}
[inst : Small α]
{f : α → β}
(hf : Function.Surjective f)
:
Small β
We don't define small_of_fintype
or small_of_countable
in this file,
to keep imports to logic
to a minimum.