/-
Copyright (c) 2021 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison

! This file was ported from Lean 3 source module data.countable.small
! leanprover-community/mathlib commit bbeb185db4ccee8ed07dc48449414ebfa39cb821
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Logic.Small.Basic
import Mathlib.Data.Countable.Defs

/-!
# All countable types are small.

That is, any countable type is equivalent to a type in any universe.
-/


universe w v

instance (priority := 100) 
small_of_countable: ∀ (α : Type v) [inst : Countable α], Small α
small_of_countable (
α: Type v
α : 
Type v: Type (v+1)
Type v) [
Countable: Sort ?u.4 → Prop
Countable 
α: Type v
α] : 
Small: Type ?u.7 → Prop
Small.{w} 
α: Type v
α :=
  let ⟨_, 
hf: Function.Injective w✝
hf⟩ := 
exists_injective_nat: ∀ (α : Sort ?u.11) [inst : Countable α], ∃ f, Function.Injective f
exists_injective_nat 
α: Type v
α
  
small_of_injective: ∀ {α : Type ?u.60} {β : Type ?u.61} [inst : Small β] {f : α → β}, Function.Injective f → Small α
small_of_injective 
hf: Function.Injective w✝
hf
#align small_of_countable 
small_of_countable: ∀ (α : Type v) [inst : Countable α], Small α
small_of_countable