mathlibdocumentation

data.equiv.denumerable

Denumerable types #

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.

@[class]
structure denumerable (α : Type u_1) :
Type u_1
• to_encodable :
• decode_inv : ∀ (n : ), ∃ (a : α) (H : a n),

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

Instances
theorem denumerable.decode_is_some (α : Type u_1) [denumerable α] (n : ) :
def denumerable.of_nat (α : Type u_1) [f : denumerable α] (n : ) :
α

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

Equations
@[simp]
theorem denumerable.decode_eq_of_nat (α : Type u_1) [denumerable α] (n : ) :
= some n)
@[simp]
theorem denumerable.of_nat_of_decode {α : Type u_1} [denumerable α] {n : } {b : α} (h : = some b) :
= b
@[simp]
theorem denumerable.encode_of_nat {α : Type u_1} [denumerable α] (n : ) :
@[simp]
theorem denumerable.of_nat_encode {α : Type u_1} [denumerable α] (a : α) :
def denumerable.eqv (α : Type u_1) [denumerable α] :
α

A denumerable type is equivalent to .

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

A type equivalent to is denumerable.

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

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

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

All denumerable types are equivalent.

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

If α is denumerable, then so is option α.

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

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

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

A denumerable collection of denumerable types is denumerable.

Equations
@[simp]
theorem denumerable.sigma_of_nat_val {α : Type u_1} [denumerable α] {γ : α → Type u_3} [Π (a : α), denumerable (γ a)] (n : ) :
@[protected, instance]
def denumerable.prod {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] :
denumerable × β)

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

Equations
@[simp]
theorem denumerable.prod_of_nat_val {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] (n : ) :
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def denumerable.ulift {α : Type u_1} [denumerable α] :

The lift of a denumerable type is denumerable.

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

The lift of a denumerable type is denumerable.

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

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

Equations

Subsets of ℕ#

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

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

Equations
theorem nat.subtype.succ_le_of_lt {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] {x y : s} (h : y < x) :
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 < xz y) :
theorem nat.subtype.lt_succ_self {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] (x : s) :
theorem nat.subtype.lt_succ_iff_le {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] {x y : s} :
x y
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
• (n + 1) =
theorem nat.subtype.of_nat_surjective_aux {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] {x : } (hx : x s) :
∃ (n : ), = x, hx⟩
theorem nat.subtype.of_nat_surjective {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] :
@[simp]
theorem nat.subtype.of_nat_range {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] :
@[simp]
theorem nat.subtype.coe_comp_of_nat_range {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] :
= s
def nat.subtype.denumerable (s : set ) [decidable_pred (λ (_x : ), _x s)] [infinite s] :

Any infinite set of naturals is denumerable.

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

An infinite encodable type is denumerable.

Equations