HepLean Documentation

Mathlib.Data.Countable.Basic

Countable types #

In this file we provide basic instances of the Countable typeclass defined elsewhere.

instance instCountableInt :

Equations

instCountableInt = ⋯

Definition in terms of `Function.Embedding` #

theorem countable_iff_nonempty_embedding {α : Sort u} :

Countable α ↔ Nonempty (α ↪ ℕ)

theorem uncountable_iff_isEmpty_embedding {α : Sort u} :

Uncountable α ↔ IsEmpty (α ↪ ℕ)

theorem nonempty_embedding_nat (α : Sort u_1) [Countable α] :

Nonempty (α ↪ ℕ)

theorem Function.Embedding.countable {α : Sort u} {β : Sort v} [Countable β] (f : α ↪ β) :

theorem Function.Embedding.uncountable {α : Sort u} {β : Sort v} [Uncountable α] (f : α ↪ β) :

Operations on `Type*`s #

instance instCountableSum {α : Type u} {β : Type v} [Countable α] [Countable β] :

Countable (α ⊕ β)

Equations

⋯ = ⋯

instance Sum.uncountable_inl {α : Type u} {β : Type v} [Uncountable α] :

Uncountable (α ⊕ β)

Equations

⋯ = ⋯

instance Sum.uncountable_inr {α : Type u} {β : Type v} [Uncountable β] :

Uncountable (α ⊕ β)

Equations

⋯ = ⋯

instance Option.instCountable {α : Type u} [Countable α] :

Countable (Option α)

Equations

⋯ = ⋯

instance WithTop.instCountable {α : Type u} [Countable α] :

Countable (WithTop α)

Equations

⋯ = ⋯

instance WithBot.instCountable {α : Type u} [Countable α] :

Countable (WithBot α)

Equations

⋯ = ⋯

instance ENat.instCountable :

Countable ℕ∞

Equations

ENat.instCountable = ⋯

instance Option.instUncountable {α : Type u} [Uncountable α] :

Uncountable (Option α)

Equations

⋯ = ⋯

instance WithTop.instUncountable {α : Type u} [Uncountable α] :

Uncountable (WithTop α)

Equations

⋯ = ⋯

instance WithBot.instUncountable {α : Type u} [Uncountable α] :

Uncountable (WithBot α)

Equations

⋯ = ⋯

instance instCountableProd {α : Type u} {β : Type v} [Countable α] [Countable β] :

Countable (α × β)

Equations

⋯ = ⋯

instance instUncountableProdOfNonempty {α : Type u} {β : Type v} [Uncountable α] [Nonempty β] :

Uncountable (α × β)

Equations

⋯ = ⋯

instance instUncountableProdOfNonempty_1 {α : Type u} {β : Type v} [Nonempty α] [Uncountable β] :

Uncountable (α × β)

Equations

⋯ = ⋯

theorem countable_left_of_prod_of_nonempty {α : Type u} {β : Type v} [Nonempty β] (h : Countable (α × β)) :

theorem countable_right_of_prod_of_nonempty {α : Type u} {β : Type v} [Nonempty α] (h : Countable (α × β)) :

theorem countable_prod_swap {α : Type u} {β : Type v} [Countable (α × β)] :

Countable (β × α)

instance instCountableSigma {α : Type u} {π : α → Type w} [Countable α] [∀ (a : α), Countable (π a)] :

Countable (Sigma π)

Equations

⋯ = ⋯

theorem Sigma.uncountable {α : Type u} {π : α → Type w} (a : α) [Uncountable (π a)] :

Uncountable (Sigma π)

instance instUncountableSigmaOfNonempty {α : Type u} {π : α → Type w} [Nonempty α] [∀ (a : α), Uncountable (π a)] :

Uncountable (Sigma π)

Equations

⋯ = ⋯

@[instance 500]

instance SetCoe.countable {α : Type u} [Countable α] (s : Set α) :

Equations

⋯ = ⋯

Operations on `Sort*`s #

instance instCountablePSum {α : Sort u} {β : Sort v} [Countable α] [Countable β] :

Countable (α ⊕' β)

Equations

⋯ = ⋯

instance instCountablePProd {α : Sort u} {β : Sort v} [Countable α] [Countable β] :

Countable (α ×' β)

Equations

⋯ = ⋯

instance instCountablePSigma {α : Sort u} {π : α → Sort w} [Countable α] [∀ (a : α), Countable (π a)] :

Countable (PSigma π)

Equations

⋯ = ⋯

instance instCountableForallOfFinite {α : Sort u} {π : α → Sort w} [Finite α] [∀ (a : α), Countable (π a)] :

Countable ((a : α) → π a)

Equations

⋯ = ⋯