bookshelf/Bookshelf/Enderton/Set/Chapter_6.lean

727 lines
24 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

import Bookshelf.Enderton.Set.Chapter_4
import Common.Logic.Basic
import Common.Nat.Basic
import Common.Set.Basic
import Common.Set.Equinumerous
import Common.Set.Intervals
import Mathlib.Data.Finset.Card
import Mathlib.Data.Set.Finite
import Mathlib.Tactic.LibrarySearch
/-! # 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`).
-/
namespace Enderton.Set.Chapter_6
/-- #### Theorem 6B
No set is equinumerous to its powerset.
-/
theorem theorem_6b (A : Set α)
: A ≉ 𝒫 A := by
rw [Set.not_equinumerous_def]
intro f hf
unfold Set.BijOn at hf
let φ := { a ∈ A | a ∉ f a }
suffices ∀ a ∈ A, f a ≠ φ by
have hφ := hf.right.right (show φ ∈ 𝒫 A by simp)
have ⟨a, ha⟩ := hφ
exact absurd ha.right (this a ha.left)
intro a ha hfa
by_cases h : a ∈ f a
· have h' := h
rw [hfa] at h
simp only [Set.mem_setOf_eq] at h
exact absurd h' h.right
· rw [Set.Subset.antisymm_iff] at hfa
have := hfa.right ⟨ha, h⟩
exact absurd this h
/-! ### Pigeonhole Principle -/
/--
A subset of a finite set of natural numbers has a max member.
-/
lemma subset_finite_max_nat {S' S : Set }
(hS : Set.Finite S) (hS' : Set.Nonempty S') (h : S' ⊆ S)
: ∃ m, m ∈ S' ∧ ∀ n, n ∈ S' → n ≤ m := by
have ⟨m, hm₁, hm₂⟩ :=
Set.Finite.exists_maximal_wrt id S' (Set.Finite.subset hS h) hS'
simp only [id_eq] at hm₂
refine ⟨m, hm₁, ?_⟩
intro n hn
match @trichotomous LT.lt _ m n with
| Or.inr (Or.inl r) => exact Nat.le_of_eq r.symm
| Or.inl r =>
have := hm₂ n hn (Nat.le_of_lt r)
exact Nat.le_of_eq this.symm
| Or.inr (Or.inr r) => exact Nat.le_of_lt r
/--
Auxiliary function to be proven by induction.
-/
lemma pigeonhole_principle_aux (n : )
: ∀ M, M ⊂ Set.Iio n →
∀ f : ,
Set.MapsTo f M (Set.Iio n) ∧ Set.InjOn f M →
¬ Set.SurjOn f M (Set.Iio n) := by
induction n with
| zero =>
intro _ hM
unfold Set.Iio at hM
simp only [Nat.zero_eq, not_lt_zero', Set.setOf_false] at hM
rw [Set.ssubset_empty_iff_false] at hM
exact False.elim hM
| succ n ih =>
intro M hM f ⟨hf_maps, hf_inj⟩ hf_surj
by_cases hM' : M = ∅
· unfold Set.SurjOn at hf_surj
rw [hM'] at hf_surj
simp only [Set.image_empty] at hf_surj
rw [Set.subset_def] at hf_surj
exact hf_surj n (show n < n + 1 by simp)
by_cases h : ¬ ∃ t, t ∈ M ∧ f t = n
-- Trivial case. `f` must not be onto if this is the case.
· have ⟨t, ht⟩ := hf_surj (show n ∈ _ by simp)
exact absurd ⟨t, ht⟩ h
-- Continue under the assumption `n ∈ ran f`.
simp only [not_not] at h
have ⟨t, ht₁, ht₂⟩ := h
-- `M ≠ ∅` so `∃ p, ∀ x ∈ M, p ≥ x`.
have ⟨p, hp₁, hp₂⟩ : ∃ p ∈ M, ∀ x, x ∈ M → p ≥ x := by
refine subset_finite_max_nat (show Set.Finite M from ?_) ?_ ?_
· have := Set.finite_lt_nat (n + 1)
exact Set.Finite.subset this (subset_of_ssubset hM)
· exact Set.nmem_singleton_empty.mp hM'
· show ∀ t, t ∈ M → t ∈ M
simp only [imp_self, forall_const]
-- `g` is a variant of `f` in which the largest element of its domain
-- (i.e. `p`) corresponds to value `n`.
let g x := if x = p then n else if x = t then f p else f x
have hg_maps : Set.MapsTo g M (Set.Iio (n + 1)) := by
intro x hx
dsimp only
by_cases hx₁ : x = p
· rw [hx₁]
simp
· rw [if_neg hx₁]
by_cases hx₂ : x = t
· rw [hx₂]
simp only [ite_true, Set.mem_Iio]
exact hf_maps hp₁
· rw [if_neg hx₂]
simp only [Set.mem_Iio]
exact hf_maps hx
have hg_inj : Set.InjOn g M := by
intro x₁ hx₁ x₂ hx₂ hf'
by_cases hc₁ : x₁ = p
· by_cases hc₂ : x₂ = p
· rw [hc₁, hc₂]
· dsimp at hf'
rw [hc₁] at hf'
simp only [ite_self, ite_true] at hf'
by_cases hc₃ : x₂ = t
· rw [if_neg hc₂, if_pos hc₃, ← ht₂] at hf'
rw [hc₁] at hx₁ ⊢
rw [hc₃] at hx₂ ⊢
exact hf_inj hx₁ hx₂ hf'.symm
· rw [if_neg hc₂, if_neg hc₃, ← ht₂] at hf'
have := hf_inj ht₁ hx₂ hf'
exact absurd this.symm hc₃
· by_cases hc₂ : x₂ = p
· rw [hc₂] at hf'
simp only [ite_self, ite_true] at hf'
by_cases hc₃ : x₁ = t
· rw [if_neg hc₁, if_pos hc₃, ← ht₂] at hf'
rw [hc₃] at hx₁ ⊢
rw [hc₂] at hx₂ ⊢
have := hf_inj hx₂ hx₁ hf'
exact this.symm
· rw [if_neg hc₁, if_neg hc₃, ← ht₂] at hf'
have := hf_inj hx₁ ht₁ hf'
exact absurd this hc₃
· dsimp only at hf'
rw [if_neg hc₁, if_neg hc₂] at hf'
by_cases hc₃ : x₁ = t
· by_cases hc₄ : x₂ = t
· rw [hc₃, hc₄]
· rw [if_pos hc₃, if_neg hc₄] at hf'
have := hf_inj hp₁ hx₂ hf'
exact absurd this.symm hc₂
· by_cases hc₄ : x₂ = t
· rw [if_neg hc₃, if_pos hc₄] at hf'
have := hf_inj hx₁ hp₁ hf'
exact absurd this hc₁
· rw [if_neg hc₃, if_neg hc₄] at hf'
exact hf_inj hx₁ hx₂ hf'
let M' := M \ {p}
have hM' : M' ⊂ Set.Iio n := by
by_cases hc : p = n
· suffices Set.Iio (n + 1) \ {n} = Set.Iio n by
have h₁ := Set.diff_ssubset_diff_left hM hp₁
conv at h₁ => right; rw [hc]
rwa [← this]
ext x
apply Iff.intro
· intro hx₁
refine Or.elim (Nat.lt_or_eq_of_lt hx₁.left) (by simp) ?_
intro hx₂
rw [hx₂] at hx₁
simp at hx₁
· intro hx₁
exact ⟨Nat.lt_trans hx₁ (by simp), Nat.ne_of_lt hx₁⟩
have hp_lt_n : p < n := by
have := subset_of_ssubset hM
have hp' : p < n + 1 := this hp₁
exact Or.elim (Nat.lt_or_eq_of_lt hp') id (absurd · hc)
rw [Set.ssubset_def]
apply And.intro
· show ∀ x, x ∈ M' → x < n
intro x hx
simp only [Set.mem_diff, Set.mem_singleton_iff] at hx
calc x
_ ≤ p := hp₂ x hx.left
_ < n := hp_lt_n
· show ¬ ∀ x, x < n → x ∈ M'
by_contra np
have := np p hp_lt_n
simp at this
-- Consider `g = f' - {⟨p, n⟩}`. This restriction will allow us to use
-- the induction hypothesis to prove `g` isn't surjective.
have ng_surj : ¬ Set.SurjOn g M' (Set.Iio n) := by
refine ih _ hM' g ⟨?_, ?_⟩
· -- `Set.MapsTo g M' (Set.Iio n)`
intro x hx
have hx₁ : x ∈ M := Set.mem_of_mem_diff hx
apply Or.elim (Nat.lt_or_eq_of_lt $ hg_maps hx₁)
· exact id
· intro hx₂
rw [← show g p = n by simp] at hx₂
exact absurd (hg_inj hx₁ hp₁ hx₂) hx.right
· -- `Set.InjOn g M'`
intro x₁ hx₁ x₂ hx₂ hg
have hx₁' : x₁ ∈ M := (Set.diff_subset M {p}) hx₁
have hx₂' : x₂ ∈ M := (Set.diff_subset M {p}) hx₂
exact hg_inj hx₁' hx₂' hg
-- We have shown `g` isn't surjective. This is another way of saying that.
have ⟨a, ha₁, ha₂⟩ : ∃ a, a < n ∧ a ∉ g '' M' := by
unfold Set.SurjOn at ng_surj
rw [Set.subset_def] at ng_surj
simp only [
Set.mem_Iio,
Set.mem_image,
not_forall,
not_exists,
not_and,
exists_prop
] at ng_surj
unfold Set.image
simp only [Set.mem_Iio, Set.mem_setOf_eq, not_exists, not_and]
exact ng_surj
-- If `g` isn't surjective then neither is `f`.
refine absurd (hf_surj $ calc a
_ < n := ha₁
_ < n + 1 := by simp) (show ↑a ∉ f '' M from ?_)
suffices g '' M = f '' M by
rw [← this]
show a ∉ g '' M
unfold Set.image at ha₂ ⊢
simp only [Set.mem_Iio, Set.mem_setOf_eq, not_exists, not_and] at ha₂ ⊢
intro x hx
by_cases hxp : x = p
· rw [if_pos hxp]
exact (Nat.ne_of_lt ha₁).symm
· refine ha₂ x ?_
exact Set.mem_diff_of_mem hx hxp
ext x
simp only [Set.mem_image, Set.mem_Iio]
apply Iff.intro
· intro ⟨y, hy₁, hy₂⟩
by_cases hc₁ : y = p
· rw [if_pos hc₁] at hy₂
rw [hy₂] at ht₂
exact ⟨t, ht₁, ht₂⟩
· rw [if_neg hc₁] at hy₂
by_cases hc₂ : y = t
· rw [if_pos hc₂] at hy₂
exact ⟨p, hp₁, hy₂⟩
· rw [if_neg hc₂] at hy₂
exact ⟨y, hy₁, hy₂⟩
· intro ⟨y, hy₁, hy₂⟩
by_cases hc₁ : y = p
· refine ⟨t, ht₁, ?_⟩
by_cases hc₂ : y = t
· rw [hc₂, ht₂] at hy₂
rw [← hc₁, ← hc₂]
simp only [ite_self, ite_true]
exact hy₂
· rw [hc₁, ← Ne.def] at hc₂
rwa [if_neg hc₂.symm, if_pos rfl, ← hc₁]
· by_cases hc₂ : y = t
· refine ⟨p, hp₁, ?_⟩
simp only [ite_self, ite_true]
rwa [hc₂, ht₂] at hy₂
· refine ⟨y, hy₁, ?_⟩
rwa [if_neg hc₁, if_neg hc₂]
/--
No natural number is equinumerous to a proper subset of itself.
-/
theorem pigeonhole_principle {n : }
: ∀ {M}, M ⊂ Set.Iio n → M ≉ Set.Iio n := by
intro M hM nM
have ⟨f, hf⟩ := nM
have := pigeonhole_principle_aux n M hM f ⟨hf.left, hf.right.left⟩
exact absurd hf.right.right this
/-- #### Corollary 6C
No finite set is equinumerous to a proper subset of itself.
-/
theorem corollary_6c [DecidableEq α] [Nonempty α]
{S S' : Set α} (hS : Set.Finite S) (h : S' ⊂ S)
: S ≉ S' := by
let T := S \ S'
have hT : S = S' (S \ S') := by
simp only [Set.union_diff_self]
exact (Set.left_subset_union_eq_self (subset_of_ssubset h)).symm
-- `hF : S' T ≈ S`.
-- `hG : S ≈ n`.
-- `hH : S' T ≈ n`.
have hF := Set.equinumerous_refl S
conv at hF => arg 1; rw [hT]
have ⟨n, hG⟩ := Set.finite_iff_equinumerous_nat.mp hS
have ⟨H, hH⟩ := Set.equinumerous_trans hF hG
-- Restrict `H` to `S'` to yield a bijection between `S'` and a proper subset
-- of `n`.
let R := (Set.Iio n) \ (H '' T)
have hR : Set.BijOn H S' R := by
refine ⟨?_, ?_, ?_⟩
· -- `Set.MapsTo H S' R`
intro x hx
refine ⟨hH.left $ Set.mem_union_left T hx, ?_⟩
unfold Set.image
by_contra nx
simp only [Finset.mem_coe, Set.mem_setOf_eq] at nx
have ⟨a, ha₁, ha₂⟩ := nx
have hc₁ : a ∈ S' T := Set.mem_union_right S' ha₁
have hc₂ : x ∈ S' T := Set.mem_union_left T hx
rw [hH.right.left hc₁ hc₂ ha₂] at ha₁
have hx₁ : {x} ⊆ S' := Set.singleton_subset_iff.mpr hx
have hx₂ : {x} ⊆ T := Set.singleton_subset_iff.mpr ha₁
have hx₃ := Set.disjoint_sdiff_right hx₁ hx₂
simp only [
Set.bot_eq_empty,
Set.le_eq_subset,
Set.singleton_subset_iff,
Set.mem_empty_iff_false
] at hx₃
· -- `Set.InjOn H S'`
intro x₁ hx₁ x₂ hx₂ h
have hc₁ : x₁ ∈ S' T := Set.mem_union_left T hx₁
have hc₂ : x₂ ∈ S' T := Set.mem_union_left T hx₂
exact hH.right.left hc₁ hc₂ h
· -- `Set.SurjOn H S' R`
show ∀ r, r ∈ R → r ∈ H '' S'
intro r hr
unfold Set.image
simp only [Set.mem_setOf_eq]
dsimp only at hr
have := hH.right.right hr.left
simp only [Set.mem_image, Set.mem_union] at this
have ⟨x, hx⟩ := this
apply Or.elim hx.left
· intro hx'
exact ⟨x, hx', hx.right⟩
· intro hx'
refine absurd ?_ hr.right
rw [← hx.right]
simp only [Set.mem_image, Finset.mem_coe]
exact ⟨x, hx', rfl⟩
intro hf
have hf₁ : S ≈ R := Set.equinumerous_trans hf ⟨H, hR⟩
have hf₂ : R ≈ Set.Iio n := by
have ⟨k, hk⟩ := Set.equinumerous_symm hf₁
exact Set.equinumerous_trans ⟨k, hk⟩ hG
refine absurd hf₂ (pigeonhole_principle ?_)
show R ⊂ Set.Iio n
apply And.intro
· show ∀ r, r ∈ R → r ∈ Set.Iio n
intro _ hr
exact hr.left
· show ¬ ∀ r, r ∈ Set.Iio n → r ∈ R
intro nr
have ⟨t, ht₁⟩ : Set.Nonempty T := Set.diff_ssubset_nonempty h
have ht₂ : H t ∈ Set.Iio n := hH.left (Set.mem_union_right S' ht₁)
have ht₃ : H t ∈ R := nr (H t) ht₂
exact absurd ⟨t, ht₁, rfl⟩ ht₃.right
/-- #### Corollary 6D (a)
Any set equinumerous to a proper subset of itself is infinite.
-/
theorem corollary_6d_a [DecidableEq α] [Nonempty α]
{S S' : Set α} (hS : S' ⊂ S) (hf : S ≈ S')
: Set.Infinite S := by
by_contra nS
simp only [Set.not_infinite] at nS
exact absurd hf (corollary_6c nS hS)
/-- #### Corollary 6D (b)
The set `ω` is infinite.
-/
theorem corollary_6d_b
: Set.Infinite (@Set.univ ) := by
let S : Set := { 2 * n | n ∈ @Set.univ }
let f x := 2 * x
suffices Set.BijOn f (@Set.univ ) S by
refine corollary_6d_a ?_ ⟨f, this⟩
rw [Set.ssubset_def]
apply And.intro
· simp
· show ¬ ∀ x, x ∈ Set.univ → x ∈ S
simp only [
Set.mem_univ,
true_and,
Set.mem_setOf_eq,
forall_true_left,
not_forall,
not_exists
]
refine ⟨1, ?_⟩
intro x nx
simp only [mul_eq_one, false_and] at nx
refine ⟨by simp, ?_, ?_⟩
· -- `Set.InjOn f Set.univ`
intro n₁ _ n₂ _ hf
match @trichotomous LT.lt _ n₁ n₂ with
| Or.inr (Or.inl r) => exact r
| Or.inl r =>
have := (Chapter_4.theorem_4n_ii n₁ n₂ 1).mp r
conv at this => left; rw [mul_comm]
conv at this => right; rw [mul_comm]
exact absurd hf (Nat.ne_of_lt this)
| Or.inr (Or.inr r) =>
have := (Chapter_4.theorem_4n_ii n₂ n₁ 1).mp r
conv at this => left; rw [mul_comm]
conv at this => right; rw [mul_comm]
exact absurd hf.symm (Nat.ne_of_lt this)
· -- `Set.SurjOn f Set.univ S`
show ∀ x, x ∈ S → x ∈ f '' Set.univ
intro x hx
unfold Set.image
simp only [Set.mem_univ, true_and, Set.mem_setOf_eq] at hx ⊢
exact hx
/-- #### Corollary 6E
Any finite set is equinumerous to a unique natural number.
-/
theorem corollary_6e [Nonempty α] (S : Set α) (hS : Set.Finite S)
: ∃! n : , S ≈ Set.Iio n := by
have ⟨n, hf⟩ := Set.finite_iff_equinumerous_nat.mp hS
refine ⟨n, hf, ?_⟩
intro m hg
match @trichotomous LT.lt _ m n with
| Or.inr (Or.inl r) => exact r
| Or.inl r =>
have hh := Set.equinumerous_symm hg
have hk := Set.equinumerous_trans hh hf
have hmn : Set.Iio m ⊂ Set.Iio n := Set.Iio_nat_lt_ssubset r
exact absurd hk (pigeonhole_principle hmn)
| Or.inr (Or.inr r) =>
have hh := Set.equinumerous_symm hf
have hk := Set.equinumerous_trans hh hg
have hnm : Set.Iio n ⊂ Set.Iio m := Set.Iio_nat_lt_ssubset r
exact absurd hk (pigeonhole_principle hnm)
/-- #### Lemma 6F
If `C` is a proper subset of a natural number `n`, then `C ≈ m` for some `m`
less than `n`.
-/
lemma lemma_6f {n : }
: ∀ {C}, C ⊂ Set.Iio n → ∃ m, m < n ∧ C ≈ Set.Iio m := by
induction n with
| zero =>
intro C hC
unfold Set.Iio at hC
simp only [Nat.zero_eq, not_lt_zero', Set.setOf_false] at hC
rw [Set.ssubset_empty_iff_false] at hC
exact False.elim hC
| succ n ih =>
have h_subset_equinumerous
: ∀ S, S ⊆ Set.Iio n →
∃ m, m < n + 1 ∧ S ≈ Set.Iio m := by
intro S hS
rw [subset_iff_ssubset_or_eq] at hS
apply Or.elim hS
· -- `S ⊂ Set.Iio n`
intro h
have ⟨m, hm⟩ := ih h
exact ⟨m, calc m
_ < n := hm.left
_ < n + 1 := by simp, hm.right⟩
· -- `S = Set.Iio n`
intro h
exact ⟨n, by simp, Set.eq_imp_equinumerous h⟩
intro C hC
by_cases hn : n ∈ C
· -- Since `C` is a proper subset of `n⁺`, the set `n⁺ - C` is nonempty.
have hC₁ : Set.Nonempty (Set.Iio (n + 1) \ C) := by
rw [Set.ssubset_def] at hC
have : ¬ ∀ x, x ∈ Set.Iio (n + 1) → x ∈ C := hC.right
simp only [Set.mem_Iio, not_forall, exists_prop] at this
exact this
-- `p` is the least element of `n⁺ - C`.
have ⟨p, hp⟩ := Chapter_4.well_ordering_nat hC₁
let C' := (C \ {n}) {p}
have hC'₁ : C' ⊆ Set.Iio n := by
show ∀ x, x ∈ C' → x ∈ Set.Iio n
intro x hx
match @trichotomous LT.lt _ x n with
| Or.inl r => exact r
| Or.inr (Or.inl r) =>
rw [r] at hx
apply Or.elim hx
· intro nx
simp at nx
· intro nx
simp only [Set.mem_singleton_iff] at nx
rw [nx] at hn
exact absurd hn hp.left.right
| Or.inr (Or.inr r) =>
apply Or.elim hx
· intro ⟨h₁, h₂⟩
have h₃ := subset_of_ssubset hC h₁
simp only [Set.mem_singleton_iff, Set.mem_Iio] at h₂ h₃
exact Or.elim (Nat.lt_or_eq_of_lt h₃) id (absurd · h₂)
· intro h
simp only [Set.mem_singleton_iff] at h
have := hp.left.left
rw [← h] at this
exact Or.elim (Nat.lt_or_eq_of_lt this)
id (absurd · (Nat.ne_of_lt r).symm)
have ⟨m, hm₁, hm₂⟩ := h_subset_equinumerous C' hC'₁
suffices C' ≈ C from
⟨m, hm₁, Set.equinumerous_trans (Set.equinumerous_symm this) hm₂⟩
-- Proves `f` is a one-to-one correspondence between `C'` and `C`.
let f x := if x = p then n else x
refine ⟨f, ?_, ?_, ?_⟩
· -- `Set.MapsTo f C' C`
intro x hx
dsimp only
by_cases hxp : x = p
· rw [if_pos hxp]
exact hn
· rw [if_neg hxp]
apply Or.elim hx
· exact fun x => x.left
· intro hx₁
simp only [Set.mem_singleton_iff] at hx₁
exact absurd hx₁ hxp
· -- `Set.InjOn f C'`
intro x₁ hx₁ x₂ hx₂ hf
dsimp only at hf
by_cases hx₁p : x₁ = p
· by_cases hx₂p : x₂ = p
· rw [hx₁p, hx₂p]
· rw [if_pos hx₁p, if_neg hx₂p] at hf
apply Or.elim hx₂
· intro nx
exact absurd hf.symm nx.right
· intro nx
simp only [Set.mem_singleton_iff] at nx
exact absurd nx hx₂p
· by_cases hx₂p : x₂ = p
· rw [if_neg hx₁p, if_pos hx₂p] at hf
apply Or.elim hx₁
· intro nx
exact absurd hf nx.right
· intro nx
simp only [Set.mem_singleton_iff] at nx
exact absurd nx hx₁p
· rwa [if_neg hx₁p, if_neg hx₂p] at hf
· -- `Set.SurjOn f C' C`
show ∀ x, x ∈ C → x ∈ f '' C'
intro x hx
simp only [
Set.union_singleton,
Set.mem_diff,
Set.mem_singleton_iff,
Set.mem_image,
Set.mem_insert_iff,
exists_eq_or_imp,
ite_true
]
by_cases nx₁ : x = n
· left
exact nx₁.symm
· right
by_cases nx₂ : x = p
· have := hp.left.right
rw [← nx₂] at this
exact absurd hx this
· exact ⟨x, ⟨hx, nx₁⟩, by rwa [if_neg]⟩
· refine h_subset_equinumerous C ?_
show ∀ x, x ∈ C → x ∈ Set.Iio n
intro x hx
unfold Set.Iio
apply Or.elim (Nat.lt_or_eq_of_lt (subset_of_ssubset hC hx))
· exact id
· intro hx₁
rw [hx₁] at hx
exact absurd hx hn
/-- #### Corollary 6G
Any subset of a finite set is finite.
-/
theorem corollary_6g {S S' : Set α} (hS : Set.Finite S) (hS' : S' ⊆ S)
: Set.Finite S' := by
rw [subset_iff_ssubset_or_eq] at hS'
apply Or.elim hS'
· intro h
rw [Set.finite_iff_equinumerous_nat] at hS
have ⟨n, F, hF⟩ := hS
-- Mirrors logic found in `corollary_6c`.
let T := S \ S'
let R := (Set.Iio n) \ (F '' T)
have hR : R ⊂ Set.Iio n := by
rw [Set.ssubset_def]
apply And.intro
· show ∀ x, x ∈ R → x ∈ Set.Iio n
intro _ hx
exact hx.left
· show ¬ ∀ x, x ∈ Set.Iio n → x ∈ R
intro nr
have ⟨t, ht₁⟩ : Set.Nonempty T := Set.diff_ssubset_nonempty h
have ht₂ : F t ∈ Set.Iio n := hF.left ht₁.left
have ht₃ : F t ∈ R := nr (F t) ht₂
exact absurd ⟨t, ht₁, rfl⟩ ht₃.right
suffices Set.BijOn F S' R by
have ⟨m, hm⟩ := lemma_6f hR
have := Set.equinumerous_trans ⟨F, this⟩ hm.right
exact Set.finite_iff_equinumerous_nat.mpr ⟨m, this⟩
refine ⟨?_, ?_, ?_⟩
· -- `Set.MapsTo f S' R`
intro x hx
dsimp only
simp only [Set.mem_diff, Set.mem_Iio, Set.mem_image, not_exists, not_and]
apply And.intro
· exact hF.left (subset_of_ssubset h hx)
· intro y hy
by_contra nf
have := hF.right.left (subset_of_ssubset h hx) hy.left nf.symm
rw [this] at hx
exact absurd hx hy.right
· -- `Set.InjOn f S'`
intro x₁ hx₁ x₂ hx₂ hf
have h₁ : x₁ ∈ S := subset_of_ssubset h hx₁
have h₂ : x₂ ∈ S := subset_of_ssubset h hx₂
exact hF.right.left h₁ h₂ hf
· -- `Set.SurjOn f S' R`
show ∀ x, x ∈ R → x ∈ F '' S'
intro x hx
have h₁ := hF.right.right
unfold Set.SurjOn at h₁
rw [Set.subset_def] at h₁
have ⟨y, hy⟩ := h₁ x hx.left
refine ⟨y, ?_, hy.right⟩
rw [← hy.right] at hx
simp only [Set.mem_image, Set.mem_diff, not_exists, not_and] at hx
by_contra ny
exact (hx.right y ⟨hy.left, ny⟩) rfl
· intro h
rwa [h]
/-- #### Exercise 6.7
Assume that `A` is finite and `f : A → A`. Show that `f` is one-to-one **iff**
`ran f = A`.
-/
theorem exercise_6_7 [DecidableEq α] [Nonempty α] {A : Set α} {f : αα}
(hA₁ : Set.Finite A) (hA₂ : Set.MapsTo f A A)
: Set.InjOn f A ↔ f '' A = A := by
apply Iff.intro
· intro hf
have hf₂ : A ≈ f '' A := by
refine ⟨f, ?_, hf, ?_⟩
· -- `Set.MapsTo f A (f '' A)`
intro x hx
simp only [Set.mem_image]
exact ⟨x, hx, rfl⟩
· -- `Set.SurjOn f A (f '' A)`
intro _ hx
exact hx
have hf₃ : f '' A ⊆ A := by
show ∀ x, x ∈ f '' A → x ∈ A
intro x ⟨a, ha₁, ha₂⟩
rw [← ha₂]
exact hA₂ ha₁
rw [subset_iff_ssubset_or_eq] at hf₃
exact Or.elim hf₃ (fun h => absurd hf₂ (corollary_6c hA₁ h)) id
· intro hf₁
sorry
/-- #### Exercise 6.8
Prove that the union of two finites sets is finite, without any use of
arithmetic.
-/
theorem exercise_6_8 {A B : Set α} (hA : Set.Finite A) (hB : Set.Finite B)
: Set.Finite (A B) := by
sorry
/-- #### Exercise 6.9
Prove that the Cartesian product of two finites sets is finite, without any use
of arithmetic.
-/
theorem exercise_6_9 {A : Set α} {B : Set β}
(hA : Set.Finite A) (hB : Set.Finite B)
: Set.Finite (Set.prod A B) := by
sorry
end Enderton.Set.Chapter_6