Countable and uncountable types

In this file we define a typeclass Countable saying that a given Sort* is countable and a typeclass Uncountable saying that a given Type* is uncountable.

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 these typeclasses. 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 α → ℕ.

Instances

• Bool.countable
• Encodable.countable
• Finite.to_countable
• Finset.countable
• List.countable
• Multiset.countable
• Prop.countable
• Prop.countable'
• Quotient.countable
• SetCoe.countable
• Subsingleton.to_countable
• Subtype.countable
• Vector.countable
• instCountableFin
• instCountableForallOfFinite
• instCountableInt
• instCountableNat
• instCountableOption
• instCountablePLift
• instCountablePNat
• instCountablePProd
• instCountablePSigma
• instCountablePSum
• instCountablePUnit
• instCountableProd
• instCountableQuotient
• instCountableSigma
• instCountableSum
• instCountableULift

theorem Countable.exists_injective_nat' {α : Sort u} [self : Countable α] : ∃ (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 = ⋯

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

• ⋯ = ⋯

Operations on Sort*s

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 500]

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

instance instCountablePUnit : Countable PUnit.{u}

Equations

• instCountablePUnit = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

instance Bool.countable : Countable Bool

Equations

• Bool.countable = ⋯

instance Prop.countable' : Countable Prop

Equations

• Prop.countable' = ⋯

@[instance 500]

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

Equations

• ⋯ = ⋯

@[instance 500]

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

Equations

• ⋯ = ⋯

Uncountable types

theorem uncountable_iff_not_countable (α : Sort u_1) : Uncountable α ↔ ¬Countable α

class Uncountable (α : Sort u_1) : Prop

A type α is uncountable if it is not countable.

• not_countable : ¬Countable α

  A type α is uncountable if it is not countable.

Instances

• Option.instUncountable
• Sum.uncountable_inl
• Sum.uncountable_inr
• instUncountablePLift
• instUncountableProdOfNonempty
• instUncountableProdOfNonempty_1
• instUncountableSigmaOfNonempty
• instUncountableULift

theorem Uncountable.not_countable {α : Sort u_1} [self : Uncountable α] : ¬Countable α

A type α is uncountable if it is not countable.

theorem not_uncountable_iff {α : Sort u} : ¬Uncountable α ↔ Countable α

theorem not_countable_iff {α : Sort u} : ¬Countable α ↔ Uncountable α

@[simp]

theorem not_uncountable {α : Sort u} [Countable α] : ¬Uncountable α

@[simp]

theorem not_countable {α : Sort u} [Uncountable α] : ¬Countable α

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

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

theorem not_injective_uncountable_countable {α : Sort u} {β : Sort v} [Uncountable α] [Countable β] (f : α → β) : ¬Function.Injective f

theorem not_surjective_countable_uncountable {α : Sort u} {β : Sort v} [Countable α] [Uncountable β] (f : α → β) : ¬Function.Surjective f

theorem uncountable_iff_forall_not_surjective {α : Sort u} [Nonempty α] : Uncountable α ↔ ∀ (f : ℕ → α), ¬Function.Surjective f

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

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

instance instUncountableULift {β : Type v} [Uncountable β] : Uncountable (ULift.{u, v} β)

Equations

• ⋯ = ⋯

instance instUncountablePLift {α : Sort u} [Uncountable α] : Uncountable (PLift α)

Equations

• ⋯ = ⋯

@[instance 100]

instance instInfiniteOfUncountable {α : Sort u} [Uncountable α] : Infinite α

Equations

• ⋯ = ⋯