Documentation

Mathlib.Data.Countable.Defs

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 #

source
class Countable (α : Sort u) :
Prop

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

Instances
source
theorem countable_iff_exists_injective (α : Sort u) :
Countable α ↔ ∃ (f : α → ℕ), Function.Injective f
source
theorem Countable.exists_injective_nat (α : Sort u) [Countable α] :
∃ (f : α → ℕ), Function.Injective f
source
instance instCountableNat :
Countable ℕ
source
theorem Function.Injective.countable {α : Sort u} {β : Sort v} [Countable β] {f : α → β} (hf : Injective f) :
Countable α
source
theorem Function.Surjective.countable {α : Sort u} {β : Sort v} [Countable α] {f : α → β} (hf : Surjective f) :
Countable β
source
theorem exists_surjective_nat (α : Sort u) [Nonempty α] [Countable α] :
∃ (f : ℕ → α), Function.Surjective f
source
theorem countable_iff_exists_surjective {α : Sort u} [Nonempty α] :
Countable α ↔ ∃ (f : ℕ → α), Function.Surjective f
source
theorem Countable.of_equiv {β : Sort v} (α : Sort u_1) [Countable α] (e : α ≃ β) :
Countable β
source
theorem Equiv.countable_iff {α : Sort u} {β : Sort v} (e : α ≃ β) :
Countable α ↔ Countable β
source
instance instCountableULift {β : Type v} [Countable β] :
Countable (ULift.{u, v} β)

Operations on Sort*s #

source
instance instCountablePLift {α : Sort u} [Countable α] :
Countable (PLift α)
source
@[instance 100]
instance Subsingleton.to_countable {α : Sort u} [Subsingleton α] :
Countable α
source
@[instance 500]
instance Subtype.countable {α : Sort u} [Countable α] {p : α → Prop} :
Countable { x : α // p x }
source
instance instCountableFin {n : ℕ} :
Countable (Fin n)
source
@[instance 100]
instance Finite.to_countable {α : Sort u} [Finite α] :
Countable α
source
instance instCountablePUnit :
Countable PUnit.{u}
source
@[instance 100]
instance Prop.countable (p : Prop) :
Countable p
source
instance Bool.countable :
Countable Bool
source
instance Prop.countable' :
Countable Prop
source
@[instance 500]
instance Quotient.countable {α : Sort u} [Countable α] {r : α → α → Prop} :
Countable (Quot r)
source
@[instance 500]
instance instCountableQuotient {α : Sort u} [Countable α] {s : Setoid α} :
Countable (Quotient s)

Uncountable types #

source
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
source
theorem uncountable_iff_not_countable (α : Sort u_1) :
Uncountable α ↔ ¬Countable α
source
theorem not_uncountable_iff {α : Sort u} :
¬Uncountable α ↔ Countable α
source
theorem not_countable_iff {α : Sort u} :
¬Countable α ↔ Uncountable α
source
@[simp]
theorem not_uncountable {α : Sort u} [Countable α] :
¬Uncountable α
source
@[simp]
theorem not_countable {α : Sort u} [Uncountable α] :
¬Countable α
source
theorem Function.Injective.uncountable {α : Sort u} {β : Sort v} [Uncountable α] {f : α → β} (hf : Injective f) :
Uncountable β
source
theorem Function.Surjective.uncountable {α : Sort u} {β : Sort v} [Uncountable β] {f : α → β} (hf : Surjective f) :
Uncountable α
source
theorem not_injective_uncountable_countable {α : Sort u} {β : Sort v} [Uncountable α] [Countable β] (f : α → β) :
¬Function.Injective f
source
theorem not_surjective_countable_uncountable {α : Sort u} {β : Sort v} [Countable α] [Uncountable β] (f : α → β) :
¬Function.Surjective f
source
theorem uncountable_iff_forall_not_surjective {α : Sort u} [Nonempty α] :
Uncountable α ↔ ∀ (f : ℕ → α), ¬Function.Surjective f
source
theorem Uncountable.of_equiv {β : Sort v} (α : Sort u_1) [Uncountable α] (e : α ≃ β) :
Uncountable β
source
theorem Equiv.uncountable_iff {α : Sort u} {β : Sort v} (e : α ≃ β) :
Uncountable α ↔ Uncountable β
source
instance instUncountableULift {β : Type v} [Uncountable β] :
Uncountable (ULift.{u, v} β)
source
instance instUncountablePLift {α : Sort u} [Uncountable α] :
Uncountable (PLift α)
source
@[instance 100]
instance instInfiniteOfUncountable {α : Sort u} [Uncountable α] :
Infinite α