data.equiv.denumerable - mathlib docs

@[class]

structure denumerable (α : Type u_1) :

Type u_1

to_encodable : encodable α
decode_inv : ∀ (n : ℕ), ∃ (a : α) (H : a ∈ encodable.decode α n), encodable.encode a = n

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

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 : ℕ) :

α

Equations

denumerable.of_nat α n = option.get _

source

@[simp]

theorem denumerable.decode_eq_of_nat (α : Type u_1) [denumerable α] (n : ℕ) :

encodable.decode α n = some (denumerable.of_nat α n)

source

@[simp]

theorem denumerable.of_nat_of_decode {α : Type u_1} [denumerable α] {n : ℕ} {b : α} (h : encodable.decode α n = 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 α] :

α ≃ ℕ

Equations

denumerable.eqv α = {to_fun := encodable.encode denumerable.to_encodable, inv_fun := denumerable.of_nat α _inst_3, left_inv := _, right_inv := _}

source

def denumerable.mk' {α : Type u_1} (e : α ≃ ℕ) :

denumerable α

Equations

denumerable.mk' e = {to_encodable := {encode := ⇑e, decode := some ∘ ⇑(e.symm), encodek := _}, decode_inv := _}

source

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

denumerable β

Equations

denumerable.of_equiv α e = {to_encodable := {encode := encodable.encode (encodable.of_equiv α e), decode := encodable.decode β (encodable.of_equiv α e), encodek := _}, decode_inv := _}

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 β] :

α ≃ β

Equations

denumerable.equiv₂ α β = (denumerable.eqv α).trans (denumerable.eqv β).symm

source

@[protected, instance]

def denumerable.nat :

denumerable ℕ

Equations

denumerable.nat = {to_encodable := encodable.nat, decode_inv := denumerable.nat._proof_1}

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 α)

Equations

denumerable.option = {to_encodable := encodable.option denumerable.to_encodable, decode_inv := _}

source

@[protected, instance]

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

denumerable (α ⊕ β)

Equations

denumerable.sum = {to_encodable := encodable.sum denumerable.to_encodable, decode_inv := _}

source

@[protected, instance]

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

denumerable (sigma γ)

Equations

denumerable.sigma = {to_encodable := encodable.sigma (λ (a : α), denumerable.to_encodable), decode_inv := _}

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 α n.unpair.fst, denumerable.of_nat (γ (denumerable.of_nat α n.unpair.fst)) n.unpair.snd⟩

source

@[protected, instance]

def denumerable.prod {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] :

denumerable (α × β)

Equations

denumerable.prod = denumerable.of_equiv (Σ (_x : α), β) (equiv.sigma_equiv_prod α β).symm

source

@[simp]

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

denumerable.of_nat (α × β) n = (denumerable.of_nat α n.unpair.fst, denumerable.of_nat β n.unpair.snd)

source

@[simp]

theorem denumerable.prod_nat_of_nat :

denumerable.of_nat (ℕ × ℕ) = nat.unpair

source

@[protected, instance]

def denumerable.int :

denumerable ℤ

Equations

denumerable.int = denumerable.mk' equiv.int_equiv_nat

source

@[protected, instance]

def denumerable.pnat :

denumerable ℕ+

Equations

denumerable.pnat = denumerable.mk' equiv.pnat_equiv_nat

source

@[protected, instance]

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

denumerable (ulift α)

Equations

denumerable.ulift = denumerable.of_equiv α equiv.ulift

source

@[protected, instance]

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

denumerable (plift α)

Equations

denumerable.plift = denumerable.of_equiv α equiv.plift

source

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

α × α ≃ α

Equations

denumerable.pair = denumerable.equiv₂ (α × α) α

source

theorem nat.subtype.exists_succ {s : set ℕ} [infinite ↥s] (x : ↥s) :

∃ (n : ℕ), x.val + n + 1 ∈ s

source

def nat.subtype.succ {s : set ℕ} [infinite ↥s] [decidable_pred s] (x : ↥s) :

↥s

Equations

nat.subtype.succ x = have h : ∃ (m : ℕ), x.val + m + 1 ∈ s, from _, ⟨x.val + nat.find h + 1, _⟩

source

theorem nat.subtype.succ_le_of_lt {s : set ℕ} [infinite ↥s] [decidable_pred 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 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 s] (x : ↥s) :

x < nat.subtype.succ x

source

theorem nat.subtype.lt_succ_iff_le {s : set ℕ} [infinite ↥s] [decidable_pred s] {x y : ↥s} :

x < nat.subtype.succ y ↔ x ≤ y

source

def nat.subtype.of_nat (s : set ℕ) [decidable_pred s] [infinite ↥s] :

ℕ → ↥s

Equations

nat.subtype.of_nat s (n + 1) = nat.subtype.succ (nat.subtype.of_nat s n)
nat.subtype.of_nat s 0 = ⊥

source

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⟩

source

theorem nat.subtype.of_nat_surjective {s : set ℕ} [infinite ↥s] [decidable_pred s] :

function.surjective (nat.subtype.of_nat s)

source

def nat.subtype.denumerable (s : set ℕ) [decidable_pred s] [infinite ↥s] :

denumerable ↥s

Equations

nat.subtype.denumerable s = denumerable.of_equiv ℕ {to_fun := to_fun_aux (λ (a : ℕ), _inst_3 a), inv_fun := nat.subtype.of_nat s _inst_4, left_inv := _, right_inv := _}

source

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

denumerable α

Equations

denumerable.of_encodable_of_infinite α = let _inst : decidable_pred (set.range encodable.encode) := encodable.decidable_range_encode α, _inst_3 : infinite ↥(set.range encodable.encode) := _, _inst_4 : denumerable ↥(set.range encodable.encode) := nat.subtype.denumerable (set.range encodable.encode) in denumerable.of_equiv ↥(set.range encodable.encode) (encodable.equiv_range_encode α)