Theory listCardinality

Parents

Contents

Type operators

(none)

Constants

list : (α -> bool) -> α list -> bool

Definitions

Theorems

COUNTABLE_LIST_UNIV COUNTABLE_LIST_UNIV'INFINITE_A_list_BIJ_A UNIV_list list_BIGUNION_EXP list_EMPTY list_SING set_exp_count

Definitions

⊢ ∀A. list A = {l | ∀e. MEM e l ⇒ e ∈ A}

Theorems

COUNTABLE_LIST_UNIV

⊢ countable 𝕌(:α) ⇒ countable 𝕌(:α list)

COUNTABLE_LIST_UNIV'

⊢ FINITE 𝕌(:α) ⇒ countable 𝕌(:α list)

INFINITE_A_list_BIJ_A

⊢ INFINITE A ⇒ list A ≈ A

⊢ 𝕌(:α list) = list 𝕌(:α)

list_BIGUNION_EXP

⊢ list A ≈ BIGUNION (IMAGE (λn. {n} × A ** count n) 𝕌(:num))

⊢ list ∅ = {[]}

⊢ list {e} ≈ 𝕌(:num)

set_exp_count

⊢ A ** count n ≈ {l | LENGTH l = n ∧ ∀e. MEM e l ⇒ e ∈ A}