def sameCardinality (A : Type u) (B : Type v) : Prop

Definition 0.3.26: Sets A and B have the same cardinality when there exists a bijection f : A → B. The cardinality |A| is the equivalence class of all sets with the same cardinality as A.

Equations

• sameCardinality A B = Nonempty (A ≃ B)

theorem sameCardinality_iff_cardinal_eq {A : Type u} {B : Type v} : sameCardinality A B ↔ Cardinal.lift.{v, u} (Cardinal.mk A) = Cardinal.lift.{u, v} (Cardinal.mk B)

The book's notion of equal cardinalities matches mathlib's equality of cardinals.

def cardinalityClass (A : Type u) : Set (Type u)

The cardinality class of a set A is the collection of all sets bijective to A.

Equations

• cardinalityClass A = {B : Type ?u.7 | sameCardinality A B}

@[reducible, inline]

abbrev cardinality (A : Type u) : Cardinal.{u}

The book's cardinality |A| corresponds to the mathlib cardinal Cardinal.mk A.

Equations

• cardinality A = Cardinal.mk A

def elementCollectionCardEq {α : Type u} (A : Set α) (n : ℕ) : Prop

Definition 0.3.27: A set has cardinality n when it is in bijection with {1, 2, …, n} (or is empty when n = 0); such sets are called finite. A set is infinite if it is not finite.

Equations

• elementCollectionCardEq A n = Nonempty (Subtype A ≃ Fin n)

@[reducible, inline]

abbrev finiteElementCollection {α : Type u} (A : Set α) : Prop

The book's notion of a finite set: it has the same cardinality as some {1, …, n}.

Equations

• finiteElementCollection A = ∃ (n : ℕ), elementCollectionCardEq A n

theorem finiteElementCollection_iff_setFinite {α : Type u} {A : Set α} : finiteElementCollection A ↔ A.Finite

The book's finite sets correspond to mathlib's Set.Finite.

@[reducible, inline]

abbrev infiniteElementCollection {α : Type u} (A : Set α) : Prop

The book's infinite sets are those that are not finite.

Equations

• infiniteElementCollection A = ¬finiteElementCollection A

theorem infiniteElementCollection_iff_setInfinite {α : Type u} {A : Set α} : infiniteElementCollection A ↔ A.Infinite

The book's infinite sets correspond to mathlib's Set.Infinite.

def cardinalLe (A : Type u) (B : Type v) : Prop

Definition 0.3.28: We write |A| ≤ |B| if there is an injection from A to B; |A| = |B| when the two have the same cardinality; |A| < |B| when |A| ≤ |B| but the cardinalities are not equal.

Equations

• cardinalLe A B = ∃ (f : A → B), Function.Injective f

theorem cardinalLe_iff {A : Type u} {B : Type v} : cardinalLe A B ↔ Cardinal.lift.{v, u} (Cardinal.mk A) ≤ Cardinal.lift.{u, v} (Cardinal.mk B)

The book's |A| ≤ |B| corresponds to the cardinal inequality of Cardinal.mk.

def cardinalLt (A : Type u) (B : Type v) : Prop

The book's strict cardinal inequality |A| < |B| means |A| ≤ |B| but not equal.

Equations

• cardinalLt A B = (cardinalLe A B ∧ ¬sameCardinality A B)

theorem cardinalLt_iff {A : Type u} {B : Type v} : cardinalLt A B ↔ Cardinal.lift.{v, u} (Cardinal.mk A) < Cardinal.lift.{u, v} (Cardinal.mk B)

The book's |A| < |B| matches the strict inequality of cardinals.

def countablyInfiniteElementCollection {α : Type u} (A : Set α) : Prop

Definition 0.3.29: A set is countably infinite if its cardinality equals that of the natural numbers; it is countable if it is finite or countably infinite; otherwise it is uncountable.

Equations

• countablyInfiniteElementCollection A = Nonempty (Subtype A ≃ ℕ)

theorem countablyInfiniteElementCollection_iff_cardinal_eq_nat {α : Type u} {A : Set α} : countablyInfiniteElementCollection A ↔ Cardinal.mk (Subtype A) = Cardinal.aleph0

def countableElementCollection {α : Type u} (A : Set α) : Prop

Equations

• countableElementCollection A = (finiteElementCollection A ∨ countablyInfiniteElementCollection A)

def uncountableElementCollection {α : Type u} (A : Set α) : Prop

Equations

• uncountableElementCollection A = ¬countableElementCollection A

theorem countableElementCollection_iff_setCountable {α : Type u} {A : Set α} : countableElementCollection A ↔ A.Countable

theorem uncountableElementCollection_iff_not_setCountable {α : Type u} {A : Set α} : uncountableElementCollection A ↔ ¬A.Countable

def evenNaturals : Set ℕ

Example 0.3.30: The set E of even natural numbers has the same cardinality as ℕ; the bijection is given by n ↦ 2n.

Equations

• evenNaturals = {n : ℕ | Even n}

theorem evenNaturals_map_bijective : Function.Bijective fun (n : ℕ) => ⟨2 * n, ⋯⟩

The map n ↦ 2n is a bijection from ℕ onto the even naturals.

theorem equiv_nat_evenNaturals : Nonempty (ℕ ≃ Subtype evenNaturals)

An explicit equivalence between ℕ and the even naturals.

theorem evenNaturals_sameCardinality_nat : sameCardinality (Subtype evenNaturals) ℕ

Example 0.3.30 (continued).

theorem natProd_countablyInfinite : countablyInfiniteElementCollection Set.univ

Example 0.3.31: The Cartesian product ℕ × ℕ is countably infinite, for example via the diagonal enumeration (1,1), (1,2), (2,1), (1,3), (2,2), (3,1), ….

theorem rat_equiv_nat : Nonempty (ℚ ≃ ℕ)

ℚ is denumerable, so we can pick an explicit equivalence with ℕ.

theorem rationals_countablyInfinite : countablyInfiniteElementCollection Set.univ

Example 0.3.32: The set of rational numbers is countable (in fact countably infinite), e.g., by enumerating positive fractions in a grid and then inserting 0 and their negatives.

@[reducible, inline]

abbrev powerSetElementCollection {α : Type u} (A : Set α) : Set (Set α)

Definition 0.3.33: The power set 𝒫(A) of a set A is the set of all subsets of A.

Equations

• powerSetElementCollection A = 𝒫 A

theorem powerSetElementCollection_eq {α : Type u} (A : Set α) : powerSetElementCollection A = 𝒫 A

The book's power set of A is mathlib's 𝒫 A.

theorem mem_powerSetElementCollection {α : Type u} {A B : Set α} : B ∈ powerSetElementCollection A ↔ B ⊆ A

Membership in the power set means being a subset.

theorem cantor_cardinal_lt (A : Type u) : Cardinal.mk A < Cardinal.mk (Set A)

Theorem 0.3.34 (Cantor). For any set A, the cardinality of A is strictly less than the cardinality of its power set 𝒫 A; in particular there is no surjection from A onto 𝒫 A.

theorem no_surjection_to_powerSet (A : Type u) (f : A → Set A) : ¬Function.Surjective f