mathlib3 documentation

logic.denumerable

Denumerable types #

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

This file defines denumerable (countably infinite) types as a typeclass extending encodable. This is used to provide explicit encode/decode functions from and to ℕ, with the information that those functions are inverses of each other.

Implementation notes #

This property already has a name, namely α ≃ ℕ, but here we are interested in using it as a typeclass.

source
@[class]
structure denumerable (α : Type u_3) :
Type u_3

A denumerable type is (constructively) bijective with ℕ. Typeclass equivalent of α ≃ ℕ.

Instances of this typeclass
Instances of other typeclasses for denumerable
  • denumerable.has_sizeof_inst
source
theorem denumerable.decode_is_some (α : Type u_1) [denumerable α] (n : ℕ) :
↥((encodable.decode α n).is_some)
source
def denumerable.of_nat (α : Type u_1) [f : denumerable α] (n : ℕ) :
α

Returns the n-th element of α indexed by the decoding.

Equations
source
@[simp]
theorem denumerable.decode_eq_of_nat (α : Type u_1) [denumerable α] (n : ℕ) :
encodable.decode α n = option.some (denumerable.of_nat α n)
source
@[simp]
theorem denumerable.of_nat_of_decode {α : Type u_1} [denumerable α] {n : ℕ} {b : α} (h : encodable.decode α n = option.some b) :
denumerable.of_nat α n = b
source
@[simp]
theorem denumerable.encode_of_nat {α : Type u_1} [denumerable α] (n : ℕ) :
encodable.encode (denumerable.of_nat α n) = n
source
@[simp]
theorem denumerable.of_nat_encode {α : Type u_1} [denumerable α] (a : α) :
denumerable.of_nat α (encodable.encode a) = a
source
def denumerable.eqv (α : Type u_1) [denumerable α] :
α ≃ ℕ

A denumerable type is equivalent to ℕ.

Equations
source
@[protected, instance]
def denumerable.infinite {α : Type u_1} [denumerable α] :
infinite α
source
def denumerable.mk' {α : Type u_1} (e : α ≃ ℕ) :
denumerable α

A type equivalent to ℕ is denumerable.

Equations
source
def denumerable.of_equiv (α : Type u_1) {β : Type u_2} [denumerable α] (e : β ≃ α) :
denumerable β

Denumerability is conserved by equivalences. This is transitivity of equivalence the denumerable way.

Equations
source
@[simp]
theorem denumerable.of_equiv_of_nat (α : Type u_1) {β : Type u_2} [denumerable α] (e : β ≃ α) (n : ℕ) :
denumerable.of_nat β n = ⇑(e.symm) (denumerable.of_nat α n)
source
def denumerable.equiv₂ (α : Type u_1) (β : Type u_2) [denumerable α] [denumerable β] :
α ≃ β

All denumerable types are equivalent.

Equations
source
@[protected, instance]
def denumerable.nat  :
denumerable ℕ
Equations
source
@[simp]
theorem denumerable.of_nat_nat (n : ℕ) :
denumerable.of_nat ℕ n = n
source
@[protected, instance]
def denumerable.option {α : Type u_1} [denumerable α] :
denumerable (option α)

If α is denumerable, then so is option α.

Equations
source
@[protected, instance]
def denumerable.sum {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] :
denumerable (α ⊕ β)

If α and β are denumerable, then so is their sum.

Equations
source
@[protected, instance]
def denumerable.sigma {α : Type u_1} [denumerable α] {γ : α → Type u_3} [Π (a : α), denumerable (γ a)] :
denumerable (sigma γ)

A denumerable collection of denumerable types is denumerable.

Equations
source
@[simp]
theorem denumerable.sigma_of_nat_val {α : Type u_1} [denumerable α] {γ : α → Type u_3} [Π (a : α), denumerable (γ a)] (n : ℕ) :
denumerable.of_nat (sigma γ) n = ⟨denumerable.of_nat α (nat.unpair n).fst, denumerable.of_nat (γ (denumerable.of_nat α (nat.unpair n).fst)) (nat.unpair n).snd⟩
source
@[protected, instance]
def denumerable.prod {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] :
denumerable (α × β)

If α and β are denumerable, then so is their product.

Equations
source
@[simp]
theorem denumerable.prod_of_nat_val {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] (n : ℕ) :
denumerable.of_nat (α × β) n = (denumerable.of_nat α (nat.unpair n).fst, denumerable.of_nat β (nat.unpair n).snd)
source
@[simp]
theorem denumerable.prod_nat_of_nat  :
denumerable.of_nat (ℕ × ℕ) = nat.unpair
source
@[protected, instance]
def denumerable.int  :
denumerable ℤ
Equations
source
@[protected, instance]
def denumerable.pnat  :
denumerable ℕ+
Equations
source
@[protected, instance]
def denumerable.ulift {α : Type u_1} [denumerable α] :
denumerable (ulift α)

The lift of a denumerable type is denumerable.

Equations
source
@[protected, instance]
def denumerable.plift {α : Type u_1} [denumerable α] :
denumerable (plift α)

The lift of a denumerable type is denumerable.

Equations
source
def denumerable.pair {α : Type u_1} [denumerable α] :
α × α ≃ α

If α is denumerable, then α × α and α are equivalent.

Equations

Subsets of ℕ #

source
theorem nat.subtype.exists_succ {s : set ℕ} [infinite ↥s] (x : ↥s) :
∃ (n : ℕ), ↑x + n + 1 ∈ s
source
def nat.subtype.succ {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] (x : ↥s) :
↥s

Returns the next natural in a set, according to the usual ordering of ℕ.

Equations
source
theorem nat.subtype.succ_le_of_lt {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] {x y : ↥s} (h : y < x) :
nat.subtype.succ y ≤ x
source
theorem nat.subtype.le_succ_of_forall_lt_le {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] {x y : ↥s} (h : ∀ (z : ↥s), z < x → z ≤ y) :
x ≤ nat.subtype.succ y
source
theorem nat.subtype.lt_succ_self {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] (x : ↥s) :
x < nat.subtype.succ x
source
theorem nat.subtype.lt_succ_iff_le {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] {x y : ↥s} :
x < nat.subtype.succ y ↔ x ≤ y
source
def nat.subtype.of_nat (s : set ℕ) [decidable_pred (λ (_x : ℕ), _x ∈ s)] [infinite ↥s] :
ℕ → ↥s

Returns the n-th element of a set, according to the usual ordering of ℕ.

Equations
source
theorem nat.subtype.of_nat_surjective_aux {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] {x : ℕ} (hx : x ∈ s) :
∃ (n : ℕ), nat.subtype.of_nat s n = ⟨x, hx⟩
source
theorem nat.subtype.of_nat_surjective {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] :
function.surjective (nat.subtype.of_nat s)
source
@[simp]
theorem nat.subtype.of_nat_range {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] :
set.range (nat.subtype.of_nat s) = set.univ
source
@[simp]
theorem nat.subtype.coe_comp_of_nat_range {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] :
set.range (coe ∘ nat.subtype.of_nat s) = s
source
def nat.subtype.denumerable (s : set ℕ) [decidable_pred (λ (_x : ℕ), _x ∈ s)] [infinite ↥s] :
denumerable ↥s

Any infinite set of naturals is denumerable.

Equations
source
def denumerable.of_encodable_of_infinite (α : Type u_1) [encodable α] [infinite α] :
denumerable α

An infinite encodable type is denumerable.

Equations
source
theorem nonempty_denumerable (α : Type u_1) [countable α] [infinite α] :
nonempty (denumerable α)

See also nonempty_encodable, nonempty_fintype.

source
@[protected, instance]
def nonempty_equiv_of_countable {α : Type u_1} {β : Type u_2} [countable α] [infinite α] [countable β] [infinite β] :
nonempty (α ≃ β)