Documentation

Mathlib.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 #

theorem countable_iff_exists_injective (α : Sort u) :

Countable α ↔ ∃ f, Function.Injective f

class Countable (α : Sort u) :

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

theorem Countable.exists_injective_nat (α : Sort u) [inst : Countable α] :

∃ f, Function.Injective f

instance instCountableNat :

Equations

instCountableNat = instCountableNat.proof_1

theorem Function.Injective.countable {α : Sort u} {β : Sort v} [inst : Countable β] {f : α → β} (hf : Function.Injective f) :

theorem Function.Surjective.countable {α : Sort u} {β : Sort v} [inst : Countable α] {f : α → β} (hf : Function.Surjective f) :

theorem exists_surjective_nat (α : Sort u) [inst : Nonempty α] [inst : Countable α] :

∃ f, Function.Surjective f

theorem countable_iff_exists_surjective {α : Sort u} [inst : Nonempty α] :

Countable α ↔ ∃ f, Function.Surjective f

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

theorem Equiv.countable_iff {α : Sort u} {β : Sort v} (e : α ≃ β) :

Countable α ↔ Countable β

instance instCountableULift {β : Type v} [inst : Countable β] :

Countable (ULift β)

Equations

@instCountableULift = @instCountableULift.proof_1

Operations on `Sort _`s #

instance instCountablePLift {α : Sort u} [inst : Countable α] :

Countable (PLift α)

Equations

@instCountablePLift = @instCountablePLift.proof_1

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

Equations

@Subsingleton.to_countable = @Subsingleton.to_countable.proof_1

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

Countable { x // p x }

Equations

@Subtype.countable = @Subtype.countable.proof_1

instance instCountableFin {n : ℕ} :

Countable (Fin n)

Equations

@instCountableFin = @instCountableFin.proof_1

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

Equations

@Finite.to_countable = @Finite.to_countable.proof_1

instance instCountablePUnit :

Countable PUnit

Equations

instCountablePUnit = (_ : Countable PUnit)

instance Prop.countable (p : Prop) :

Equations

Prop.countable = Prop.countable.proof_1

instance Bool.countable :

Equations

Bool.countable = Bool.countable.proof_1

instance Prop.countable' :

Equations

Prop.countable' = Prop.countable'.proof_1

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

Countable (Quot r)

Equations

@Quotient.countable = @Quotient.countable.proof_1

instance instCountableQuotient {α : Sort u} [inst : Countable α] {s : Setoid α} :

Countable (Quotient s)

Equations

@instCountableQuotient = @instCountableQuotient.proof_1