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

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

• exists_injective_nat' : ∃ (f : α → ℕ), Function.Injective f

  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 ℕ

Equations

• 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} β)

Equations

• (_ : Countable (ULift.{u, v} β)) = (_ : Countable (ULift.{u, v} β))

Operations on Sort*s

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

Equations

• (_ : Countable (PLift α)) = (_ : Countable (PLift α))

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

Equations

• (_ : Countable α) = (_ : Countable α)

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

Equations

• (_ : Countable { x : α // p x }) = (_ : Countable { x : α // p x })

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

Equations

• (_ : Countable (Fin n)) = (_ : Countable (Fin n))

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

Equations

• (_ : Countable α) = (_ : Countable α)

instance instCountablePUnit : Countable PUnit.{u}

Equations

• instCountablePUnit = (_ : Countable PUnit.{u})

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

Equations

• (_ : Countable p) = (_ : Countable p)

instance Bool.countable : Countable Bool

Equations

• Bool.countable = (_ : Countable Bool)

instance Prop.countable' : Countable Prop

Equations

• Prop.countable' = (_ : Countable Prop)

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

Equations

• (_ : Countable (Quot r)) = (_ : Countable (Quot r))

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

Equations

• (_ : Countable (Quotient s)) = (_ : Countable (Quot Setoid.r))