mathlib3 documentation

data.countable.defs

Countable types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
theorem countable_iff_exists_injective (α : Sort u) :
countable α ↔ ∃ (f : α → ℕ), function.injective f
source
@[class]
structure countable (α : Sort u) :
Prop

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

Instances of this typeclass
source
@[protected, instance]
def nat.countable  :
countable ℕ
source
@[protected]
theorem function.injective.countable {α : Sort u} {β : Sort v} [countable β] {f : α → β} (hf : function.injective f) :
countable α
source
@[protected]
theorem function.surjective.countable {α : Sort u} {β : Sort v} [countable α] {f : α → β} (hf : function.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
@[protected, instance]
def ulift.countable {β : Type v} [countable β] :
countable (ulift β)

Operations on Sort*s #

source
@[protected, instance]
def plift.countable {α : Sort u} [countable α] :
countable (plift α)
source
@[protected, instance]
def subsingleton.to_countable {α : Sort u} [subsingleton α] :
countable α
source
@[protected, instance]
def subtype.countable {α : Sort u} [countable α] {p : α → Prop} :
countable {x // p x}
source
@[protected, instance]
def fin.countable {n : ℕ} :
countable (fin n)
source
@[protected, instance]
def finite.to_countable {α : Sort u} [finite α] :
countable α
source
@[protected, instance]
def punit.countable  :
countable punit
source
@[protected, nolint, instance]
def Prop.countable (p : Prop) :
countable p
source
@[protected, instance]
def bool.countable  :
countable bool
source
@[protected, instance]
def Prop.countable'  :
countable Prop
source
@[protected, instance]
def quot.countable {α : Sort u} [countable α] {r : α → α → Prop} :
countable (quot r)
source
@[protected, instance]
def quotient.countable {α : Sort u} [countable α] {s : setoid α} :
countable (quotient s)