mathlib documentation

data.countable.defs

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 #

@[protected, instance]
@[protected]
theorem function.injective.countable {α : Sort u} {β : Sort v} [countable β] {f : α β} (hf : function.injective f) :
@[protected]
theorem function.surjective.countable {α : Sort u} {β : Sort v} [countable α] {f : α β} (hf : function.surjective f) :
theorem countable.of_equiv {β : Sort v} (α : Sort u_1) [countable α] (e : α β) :
theorem equiv.countable_iff {α : Sort u} {β : Sort v} (e : α β) :
@[protected, instance]
def ulift.countable {β : Type v} [countable β] :

Operations on Sort*s #

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