Countable types

In this file we define a typeclass saying that a given Sort* is countable. See also Encodable for a version that singles out a specific encoding of elements of α by natural numbers.

This file also provides a few instances of this typeclass. More instances can be found in other files.

Definition and basic properties

theorem countable_iff_exists_injective (α : Sort u) : Countable α ↔ ∃ f, Function.Injective f

class Countable (α : Sort u) : Prop

• exists_injective_nat' : ∃ f, Function.Injective f

  A type α is countable if there exists an injective map α → ℕ.

A type α is countable if there exists an injective map α → ℕ.

theorem Countable.exists_injective_nat (α : Sort u) [Countable α] : ∃ f, Function.Injective f

instance instCountableNat : Countable ℕ

theorem Function.Injective.countable {α : Sort u} {β : Sort v} [Countable β] {f : α → β} (hf : Function.Injective f) : Countable α

theorem Function.Surjective.countable {α : Sort u} {β : Sort v} [Countable α] {f : α → β} (hf : Function.Surjective f) : Countable β

theorem exists_surjective_nat (α : Sort u) [Nonempty α] [Countable α] : ∃ f, Function.Surjective f

theorem countable_iff_exists_surjective {α : Sort u} [Nonempty α] : Countable α ↔ ∃ f, Function.Surjective f

theorem Countable.of_equiv {β : Sort v} (α : Sort u_1) [Countable α] (e : α ≃ β) : Countable β

theorem Equiv.countable_iff {α : Sort u} {β : Sort v} (e : α ≃ β) : Countable α ↔ Countable β

instance instCountableULift {β : Type v} [Countable β] : Countable (ULift.{u, v} β)

Operations on Sort*s

instance instCountablePLift {α : Sort u} [Countable α] : Countable (PLift α)

instance Subsingleton.to_countable {α : Sort u} [Subsingleton α] : Countable α

instance Subtype.countable {α : Sort u} [Countable α] {p : α → Prop} : Countable { x // p x }

instance instCountableFin {n : ℕ} : Countable (Fin n)

instance Finite.to_countable {α : Sort u} [Finite α] : Countable α

instance instCountablePUnit : Countable PUnit.{u}

instance Prop.countable (p : Prop) : Countable p

instance Bool.countable : Countable Bool

instance Prop.countable' : Countable Prop

instance Quotient.countable {α : Sort u} [Countable α] {r : α → α → Prop} : Countable (Quot r)

instance instCountableQuotient {α : Sort u} [Countable α] {s : Setoid α} : Countable (Quotient s)