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.1 Show that the equation ``` f(m, n) = 2ᵐ(2n + 1) - 1 ``` defines a one-to-one correspondence between `ω × ω` and `ω`. -/ theorem exercise_6_1 : Function.Bijective (fun p : ℕ × ℕ => 2 ^ p.1 * (2 * p.2 + 1) - 1) := by sorry /-- #### Exercise 6.2 Show that in Fig. 32 we have: ``` J(m, n) = [1 + 2 + ⋯ + (m + n)] + m = (1 / 2)[(m + n)² + 3m + n]. ``` -/ theorem exercise_6_2 : Function.Bijective (fun p : ℕ × ℕ => (1 / 2) * ((p.1 + p.2) ^ 2 + 3 * p.1 + p.2)) := by sorry /-- #### Exercise 6.3 Find a one-to-one correspondence between the open unit interval `(0, 1)` and `ℝ` that takes rationals to rationals and irrationals to irrationals. -/ theorem exercise_6_3 : True := by sorry /-- #### Exercise 6.4 Construct a one-to-one correspondence between the closed unit interval ``` [0, 1] = {x ∈ ℝ | 0 ≤ x ≤ 1} ``` and the open unit interval `(0, 1)`. -/ theorem exercise_6_4 : ∃ F, Set.BijOn F (Set.Ioo 0 1) (@Set.univ ℝ) := by sorry end Enderton.Set.Chapter_6