Enderton.Set.Chapter_6

Cardinal Numbers and the Axiom of Choice

NOTE: We choose to use injectivity/surjectivity concepts found in Mathlib.Data.Set.Function over those in Mathlib.Init.Function since the former provides noncomputable utilities around obtaining inverse functions (namely Function.invFunOn).

theorem Enderton.Set.Chapter_6.theorem_6b {α : Type u_1} (A : Set α) : A ≉ 𝒫 A

Theorem 6B

No set is equinumerous to its powerset.

Pigeonhole Principle

theorem Enderton.Set.Chapter_6.subset_finite_max_nat {S' : Set ℕ} {S : Set ℕ} (hS : Set.Finite S) (hS' : Set.Nonempty S') (h : S' ⊆ S) : ∃ m ∈ S', ∀ n ∈ S', n ≤ m

A subset of a finite set of natural numbers has a max member.

theorem Enderton.Set.Chapter_6.pigeonhole_principle_aux (n : ℕ) (M : Set ℕ) : M ⊂ Set.Iio n → ∀ (f : ℕ → ℕ), Set.MapsTo f M (Set.Iio n) ∧ Set.InjOn f M → ¬Set.SurjOn f M (Set.Iio n)

Auxiliary function to be proven by induction.

theorem Enderton.Set.Chapter_6.pigeonhole_principle {n : ℕ} {M : Set ℕ} : M ⊂ Set.Iio n → M ≉ Set.Iio n

No natural number is equinumerous to a proper subset of itself.

theorem Enderton.Set.Chapter_6.corollary_6c {α : Type u_1} [DecidableEq α] [Nonempty α] {S : Set α} {S' : Set α} (hS : Set.Finite S) (h : S' ⊂ S) : S ≉ S'

Corollary 6C

No finite set is equinumerous to a proper subset of itself.

theorem Enderton.Set.Chapter_6.corollary_6d_a {α : Type u_1} [DecidableEq α] [Nonempty α] {S : Set α} {S' : Set α} (hS : S' ⊂ S) (hf : S ≈ S') : Set.Infinite S

Corollary 6D (a)

Any set equinumerous to a proper subset of itself is infinite.

theorem Enderton.Set.Chapter_6.corollary_6d_b : Set.Infinite Set.univ

Corollary 6D (b)

The set ω is infinite.

theorem Enderton.Set.Chapter_6.corollary_6e {α : Type u_1} [Nonempty α] (S : Set α) (hS : Set.Finite S) : ∃! (n : ℕ), S ≈ Set.Iio n

Corollary 6E

Any finite set is equinumerous to a unique natural number.

theorem Enderton.Set.Chapter_6.lemma_6f {n : ℕ} {C : Set ℕ} : C ⊂ Set.Iio n → ∃ m < n, C ≈ Set.Iio m

Lemma 6F

If C is a proper subset of a natural number n, then C ≈ m for some m less than n.

theorem Enderton.Set.Chapter_6.corollary_6g {α : Type u_1} {S : Set α} {S' : Set α} (hS : Set.Finite S) (hS' : S' ⊆ S) : Set.Finite S'

Corollary 6G

Any subset of a finite set is finite.

theorem Enderton.Set.Chapter_6.subset_size {α : Type u_1} [DecidableEq α] [Nonempty α] {A : Set α} {B : Set α} (hBA : B ⊆ A) (hA : Set.Finite A) : ∃ (m : ℕ) (n : ℕ), B ≈ Set.Iio m ∧ A ≈ Set.Iio n ∧ m ≤ n

Subset Size

Let A be a finite set and B ⊂ A. Then there exist natural numbers m, n ∈ ω such that B ≈ m, A ≈ n, and m ≤ n.

theorem Enderton.Set.Chapter_6.finite_dom_ran_size {α : Type u_1} {f : α → α} [Nonempty α] {A : Set α} {B : Set α} (hA : Set.Finite A) (hB : Set.Finite B) (hf : Set.MapsTo f A B) : ∃ (m : ℕ) (n : ℕ), A ≈ Set.Iio m ∧ f '' A ≈ Set.Iio n ∧ m ≥ n

Finite Domain and Range Size

Let A and B be finite sets and f : A → B be a function. Then there exist natural numbers m, n ∈ ω such that dom f ≈ m, ran f ≈ n, and m ≥ n.

theorem Enderton.Set.Chapter_6.sdiff_size_aux {α : Type u_1} {m : ℕ} [DecidableEq α] [Nonempty α] (A : Set α) : A ≈ Set.Iio m → ∀ B ⊆ A, ∃ n ≤ m, B ≈ Set.Iio n ∧ A \ B ≈ Set.Iio m \ Set.Iio n

Set Difference Size

Let A ≈ m for some natural number m and B ⊆ A. Then there exists some n ∈ ω such that B ≈ n and A - B ≈ m - n.

theorem Enderton.Set.Chapter_6.sdiff_size {α : Type u_1} {m : ℕ} [DecidableEq α] [Nonempty α] {A : Set α} {B : Set α} (hB : B ⊆ A) (hA : A ≈ Set.Iio m) : ∃ n ≤ m, B ≈ Set.Iio n ∧ A \ B ≈ Set.Iio m \ Set.Iio n

theorem Enderton.Set.Chapter_6.exercise_6_7 {α : Type u_1} [DecidableEq α] [Nonempty α] {A : Set α} {f : α → α} (hA₁ : Set.Finite A) (hA₂ : Set.MapsTo f A A) : Set.InjOn f A ↔ f '' A = A

Exercise 6.7

Assume that A is finite and f : A → A. Show that f is one-to-one iff ran f = A.

theorem Enderton.Set.Chapter_6.exercise_6_8 {α : Type u_1} {A : Set α} {B : Set α} (hA : Set.Finite A) (hB : Set.Finite B) : Set.Finite (A ∪ B)

Exercise 6.8

Prove that the union of two finites sets is finite, without any use of arithmetic.

theorem Enderton.Set.Chapter_6.exercise_6_9 {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} (hA : Set.Finite A) (hB : Set.Finite B) : Set.Finite (Set.prod A B)

Exercise 6.9

Prove that the Cartesian product of two finites sets is finite, without any use of arithmetic.