mathlib documentation

data.equiv.denumerable

@[class]
structure denumerable  :
Type u_1Type u_1

A denumerable type is one which is (constructively) bijective with ℕ. Although we already have a name for this property, namely α ≃ ℕ, we are here interested in using it as a typeclass.

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

def denumerable.of_nat (α : Type u_1) [f : denumerable α] :
→ α

Equations
@[simp]
theorem denumerable.decode_eq_of_nat (α : Type u_1) [denumerable α] (n : ) :

@[simp]
theorem denumerable.of_nat_of_decode {α : Type u_1} [denumerable α] {n : } {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.mk' {α : Type u_1} :
α denumerable α

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

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

def denumerable.equiv₂ (α : Type u_1) (β : Type u_2) [denumerable α] [denumerable β] :
α β

Equations
@[instance]

Equations
@[simp]

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

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

Equations
@[simp]
theorem denumerable.sigma_of_nat_val {α : Type u_1} [denumerable α] {γ : α → Type u_3} [Π (a : α), denumerable (γ a)] (n : ) :

@[instance]
def denumerable.prod {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] :
denumerable × β)

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

@[instance]
def denumerable.ulift {α : Type u_1} [denumerable α] :

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

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

Equations
theorem nat.subtype.exists_succ {s : set } [infinite s] (x : s) :
∃ (n : ), x.val + n + 1 s

Equations
theorem nat.subtype.succ_le_of_lt {s : set } [infinite s] [decidable_pred s] {x y : s} :
y < xnat.subtype.succ y x

theorem nat.subtype.le_succ_of_forall_lt_le {s : set } [infinite s] [decidable_pred s] {x y : s} :
(∀ (z : s), z < xz y)x nat.subtype.succ y

theorem nat.subtype.of_nat_surjective_aux {s : set } [infinite s] [decidable_pred s] {x : } (hx : x s) :
∃ (n : ), nat.subtype.of_nat s n = x, hx⟩

Equations