From 7959c474a066c52974a3c597f834b3caa986c4fe Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 14 Sep 2023 13:50:22 -0600 Subject: [PATCH] Enderton (set). Fixup the pigeonhole principle. --- Bookshelf/Enderton/Set.tex | 80 ++-- Bookshelf/Enderton/Set/Chapter_4.lean | 4 +- Bookshelf/Enderton/Set/Chapter_6.lean | 605 ++++++++++++++------------ Common/Real/Floor.lean | 2 +- Common/Set/Basic.lean | 29 +- Common/Set/Finite.lean | 45 ++ 6 files changed, 453 insertions(+), 312 deletions(-) create mode 100644 Common/Set/Finite.lean diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 9fdb284..8f46ca8 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -217,7 +217,10 @@ A set is \textbf{finite} if and only if it is \nameref{ref:equinumerous} to a \nameref{ref:natural-number}. - \lean*{Mathlib/Data/Set/Finite} + \code*{Common/Set/Finite} + {Set.finite\_iff\_equinumerous\_nat} + + \lean{Mathlib/Data/Set/Finite} {Set.Finite} \section{\defined{Function}}% @@ -8770,14 +8773,14 @@ \end{enumerate} \end{theorem} - \code{Bookshelf/Enderton/Set/Chapter\_6} - {Enderton.Set.Chapter\_6.theorem\_6a\_a} + \code{Common/Set/Finite} + {Set.equinumerous\_refl} - \code{Bookshelf/Enderton/Set/Chapter\_6} - {Enderton.Set.Chapter\_6.theorem\_6a\_b} + \code{Common/Set/Finite} + {Set.equinumerous\_symm} - \code{Bookshelf/Enderton/Set/Chapter\_6} - {Enderton.Set.Chapter\_6.theorem\_6a\_c} + \code{Common/Set/Finite} + {Set.equinumerous\_trans} \begin{proof} @@ -8857,14 +8860,17 @@ \code{Bookshelf/Enderton/Set/Chapter\_6} {Enderton.Set.Chapter\_6.pigeonhole\_principle} + \lean{Mathlib/Data/Finset/Card} + {Finset.exists\_ne\_map\_eq\_of\_card\_lt\_of\_maps\_to} + \begin{proof} Let \begin{equation} \hyperlabel{sub:pigeonhole-principle-eq1} S = \{n \in \omega \mid - \forall m \in n, \text{every one-to-one function } - f \colon m \rightarrow n \text{ is not onto}\}. + \forall M \subset n, \text{every one-to-one function } + f \colon M \rightarrow n \text{ is not onto}\}. \end{equation} We show that (i) $0 \in S$ and (ii) if $n \in S$, then so is $n^+$. Afterward we prove (iii) the theorem statement. @@ -8872,20 +8878,20 @@ \paragraph{(i)}% \hyperlabel{par:pigeonhole-principle-i} - By \nameref{sub:zero-least-natural-number}, $0$ is the least natural - number. - Therefore, $0 \in S$ vacuously. + By definition, $0 = \emptyset$. + Then $0$ has no proper subsets. + Hence $0 \in S$ vacuously. \paragraph{(ii)}% \hyperlabel{par:pigeonhole-principle-ii} - Suppose $n \in S$ and let $m \in n^+$. - Furthermore, let $f \colon m \rightarrow n^+$ be a one-to-one - \nameref{ref:function} (as proof of a one-to-one function's existence, - just consider the identity function). - If $m = 0$, it vacuously holds that $f$ is not onto $n^+$. - If $m \neq 0$, \nameref{sub:theorem-4c} shows there exists some $p$ such - that $p^+ = m$. + Suppose $n \in S$ and $M \subset n^+$. + Furthermore, let $f \colon M \rightarrow n^+$ be a one-to-one + \nameref{ref:function}. + If $M = \emptyset$, it vacuously holds that $f$ is not onto $n^+$. + Otherwise $M \neq \emptyset$. + Because $M$ is finite, the \nameref{sub:trichotomy-law-natural-numbers} + implies the existence of a largest member $p \in M$. There are two cases to consider: \subparagraph{Case 1}% @@ -8896,8 +8902,8 @@ \subparagraph{Case 2}% Suppose $n \in \ran{f}$. - Then there exists some $t \in m$ such that $\tuple{t, n} \in f$. - Define $f' \colon m \rightarrow n^+$ given by + Then there exists some $t \in M$ such that $\tuple{t, n} \in f$. + Define $f' \colon M \rightarrow n^+$ given by \begin{align*} f'(p) & = f(t) = n \\ f'(t) & = f(p) \\ @@ -8906,18 +8912,17 @@ That is, $f'$ is a variant of $f$ in which the largest element of its domain (i.e. $p$) corresponds to value $n$. Next define $g = f' - \{\tuple{p, n}\}$. - Then $g$ is a function from $p$ to $n$. + Then $g$ is a function mapping $M - \{p\}$ to $n$. Since $f$ is one-to-one, $f'$ and $g$ are also one-to-one. - Since $p \in m \in n$, \nameref{sub:theorem-4f} implies $p \in n$. - Thus \eqref{sub:pigeonhole-principle-eq1} indicates $g$ must not be onto + Then \eqref{sub:pigeonhole-principle-eq1} indicates $g$ must not be onto $n$. - In other words, there exists some $a \in n$ such that - $a \not\in \ran{g}$. - Hence $a \not\in \ran{f'}$ and, consequently, $a \not\in \ran{f}$. - But $a \in n \in n^+$ meaning, by another application of - \nameref{sub:theorem-4f}, $a \in n^+$. - Therefore $f$ is not onto $n^+$. + That is, there exists some $a \in n$ such that $a \not\in \ran{g}$. + By the \nameref{sub:trichotomy-law-natural-numbers}, $a \neq n$. + Therefore $a \not\in \ran{f'}$. + $\ran{f'} = \ran{f}$ meaning $a \not\in \ran{f}$. + Because $a \in n \in n^+$, \nameref{sub:theorem-4f} implies $a \in n^+$. + Hence $f$ is not onto $n^+$. \subparagraph{Subconclusion}% @@ -8937,26 +8942,29 @@ \end{proof} -\subsection{\pending{Corollary 6C}}% +\subsection{\verified{Corollary 6C}}% \hyperlabel{sub:corollary-6c} \begin{corollary}[6C] No finite set is equinumerous to a proper subset of itself. \end{corollary} + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.corollary\_6c} + \begin{proof} Let $S$ be a \nameref{ref:finite-set} and $S'$ be a \nameref{ref:proper-subset} $S'$ of $S$. - Then there exists some nonempty set $T$, disjoint from $S'$, such that + Then there exists some set $T$, disjoint from $S'$, such that $S' \cup T = S$. - By definition of a finite set, $S$ is \nameref{ref:equinumerous} to a - natural number $n$. + By definition of a \nameref{ref:finite-set}, $S$ is + \nameref{ref:equinumerous} to a natural number $n$. By \nameref{sub:theorem-6a}, $\equinumerous{S' \cup T}{S}$ which, by the same theorem, implies $\equinumerous{S' \cup T}{n}$. Let $f$ be a one-to-one correspondence between $S' \cup T$ and $n$. - Since $T$ is nonempty, $f \restriction S'$ is a one-to-one correspondence - between $S'$ and a proper subset of $n$. + Then $f \restriction S'$ is a one-to-one correspondence between $S'$ and a + proper subset of $n$. By the \nameref{sub:pigeonhole-principle}, $n$ is not equinumerous to any proper subset of itself. Therefore \nameref{sub:theorem-6a} implies $S'$ cannot be equinumerous to diff --git a/Bookshelf/Enderton/Set/Chapter_4.lean b/Bookshelf/Enderton/Set/Chapter_4.lean index 579f63d..4ea7bfb 100644 --- a/Bookshelf/Enderton/Set/Chapter_4.lean +++ b/Bookshelf/Enderton/Set/Chapter_4.lean @@ -389,7 +389,7 @@ theorem corollary_4p_i (m n p : ℕ) (h : m + p = n + p) Let `A` be a nonempty subset of `ω`. Then there is some `m ∈ A` such that `m ≤ n` for all `n ∈ A`. -/ -theorem well_ordering_nat (A : Set ℕ) (hA : Set.Nonempty A) +theorem well_ordering_nat {A : Set ℕ} (hA : Set.Nonempty A) : ∃ m ∈ A, ∀ n, n ∈ A → m ≤ n := by -- Assume `A` does not have a least element. by_contra nh @@ -453,7 +453,7 @@ theorem strong_induction_principle_nat (A : Set ℕ) exact h'.symm by_contra nh - have ⟨m, hm⟩ := well_ordering_nat A.compl (Set.nmem_singleton_empty.mp nh) + have ⟨m, hm⟩ := well_ordering_nat (Set.nmem_singleton_empty.mp nh) refine absurd (h m ?_) hm.left -- Show that every number less than `m` is in `A`. diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean index dcf16ff..609d2bc 100644 --- a/Bookshelf/Enderton/Set/Chapter_6.lean +++ b/Bookshelf/Enderton/Set/Chapter_6.lean @@ -1,47 +1,23 @@ import Common.Logic.Basic import Common.Nat.Basic -import Mathlib.Data.Finset.Basic +import Common.Set.Basic +import Common.Set.Finite +import Mathlib.Data.Finset.Card import Mathlib.Data.Set.Finite -import Mathlib.Data.Set.Function -import Mathlib.Data.Rel -import Mathlib.Tactic.Ring -import Std.Data.Fin.Lemmas +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 6A - -For any sets `A`, `B`, and `C`, - -(a) `A ≈ A`. -(b) If `A ≈ B`, then `B ≈ A`. -(c) If `A ≈ B` and `B ≈ C`, then `A ≈ C`. --/ - -theorem theorem_6a_a (A : Set α) - : ∃ F, Set.BijOn F A A := by - refine ⟨fun x => x, ?_⟩ - unfold Set.BijOn Set.MapsTo Set.InjOn Set.SurjOn - simp only [imp_self, implies_true, Set.image_id', true_and] - exact Eq.subset rfl - -theorem theorem_6a_b [Nonempty α] (A : Set α) (B : Set β) - (F : α → β) (hF : Set.BijOn F A B) - : ∃ G, Set.BijOn G B A := by - refine ⟨Function.invFunOn F A, ?_⟩ - exact (Set.bijOn_comm $ Set.BijOn.invOn_invFunOn hF).mpr hF - -theorem theorem_6a_c (A : Set α) (B : Set β) (C : Set γ) - (F : α → β) (hF : Set.BijOn F A B) - (G : β → γ) (hG : Set.BijOn G B C) - : ∃ H, Set.BijOn H A C := by - exact ⟨G ∘ F, Set.BijOn.comp hG hF⟩ - /-- #### Theorem 6B No set is equinumerous to its powerset. @@ -65,273 +41,366 @@ theorem theorem_6b (A : Set α) have := hfa.right ⟨ha, h⟩ exact absurd this h -/-! #### Pigeonhole Principle +/-! ### Pigeonhole Principle -/ -No natural number is equinumerous to a proper subset of itself. +/-- +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 < n → - ∀ f : Fin m → Fin n, Function.Injective f → - ¬ Function.Surjective f := by + : ∀ 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 - simp at hm + 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_inj hf_surj + intro M hM f ⟨hf_maps, hf_inj⟩ hf_surj - by_cases hm' : m = 0 - · have ⟨a, ha⟩ := hf_surj 0 - rw [hm'] at a - have := a.isLt - simp only [not_lt_zero'] at this + 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) - -- `m ≠ 0` so `∃ p, p + 1 = m`. Represent as both a `ℕ` and `Fin` type. - have ⟨nat_p, hnat_p⟩ := Nat.exists_eq_succ_of_ne_zero hm' - have hnat_p_lt_m : nat_p < m := calc nat_p - _ < nat_p + 1 := by simp - _ = m := hnat_p.symm - let fin_p : Fin m := ⟨nat_p, hnat_p_lt_m⟩ - - by_cases hn : ¬ ∃ t, f t = n + by_cases h : ¬ ∃ t, t ∈ M ∧ f t = n -- Trivial case. `f` must not be onto if this is the case. - · exact absurd (hf_surj n) hn + · 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 hn - have ⟨fin_t, hfin_t⟩ := hn + simp only [not_not] at h + have ⟨t, ht₁, ht₂⟩ := h - -- `f'` is a variant of `f` in which the largest element of its domain + -- `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 f' : Fin m → Fin (n + 1) := fun x => - if x = fin_p then n - else if x = fin_t then f fin_p - else f x + let g x := if x = p then n else if x = t then f p else f x - have hf'_inj : Function.Injective f' := by - intro x₁ x₂ hf' - by_cases hx₁ : x₁ = fin_p - · by_cases hx₂ : x₂ = fin_p - · rw [hx₁, hx₂] - · rw [hx₁] at hf' + 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 ht : x₂ = fin_t - · rw [if_neg hx₂, if_pos ht, ← hfin_t] at hf' - have := (hf_inj hf').symm - rwa [hx₁, ht] - · rw [if_neg hx₂, if_neg ht, ← hfin_t] at hf' - have := (hf_inj hf').symm - exact absurd this ht - · by_cases hx₂ : x₂ = fin_p - · rw [hx₂] 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 ht : x₁ = fin_t - · rw [if_neg hx₁, if_pos ht, ← hfin_t] at hf' - have := (hf_inj hf').symm - rw [← ht] at this - exact absurd this hx₁ - · rw [if_neg hx₁, if_neg ht, ← hfin_t] at hf' - have := hf_inj hf' - exact absurd this ht + 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 hx₁, if_neg hx₂] at hf' - by_cases ht₁ : x₁ = fin_t - · by_cases ht₂ : x₂ = fin_t - · rw [ht₁, ht₂] - · rw [if_pos ht₁, if_neg ht₂] at hf' - have := (hf_inj hf').symm - exact absurd this hx₂ - · by_cases ht₂ : x₂ = fin_t - · rw [if_neg ht₁, if_pos ht₂] at hf' - have := hf_inj hf' - exact absurd this hx₁ - · rw [if_neg ht₁, if_neg ht₂] at hf' - exact hf_inj 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' - -- `g = f' - {⟨p, n⟩}`. This restriction allows us to use the induction - -- hypothesis to prove `g` isn't surjective. - let g : Fin nat_p → Fin n := fun x => - let hxm := calc ↑x - _ < nat_p := x.isLt - _ < m := hnat_p_lt_m - let y := f' ⟨x, hxm⟩ - ⟨y, by - suffices y ≠ ↑n by - apply Or.elim (Nat.lt_or_eq_of_lt y.isLt) - · simp - · intro hy - rw [← Fin.val_ne_iff] at this - refine absurd ?_ this - rw [hy] - simp only [Fin.coe_ofNat_eq_mod] - exact Eq.symm (Nat.mod_succ_eq_iff_lt.mpr (by simp)) - by_contra ny - have hp₁ : f' fin_p = f' ⟨↑x, hxm⟩ := by - rw [show f' fin_p = n by simp, ← ny] - have hp₂ := Fin.val_eq_of_eq (hf'_inj hp₁) - exact (lt_self_iff_false ↑x).mp $ calc ↑x - _ < nat_p := x.isLt - _ = ↑fin_p := by simp - _ = ↑x := hp₂⟩ + 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 hg_inj : Function.Injective g := by - intro x₁ x₂ hg - simp only [Fin.mk.injEq] at hg - rw [if_neg (Nat.ne_of_lt x₁.isLt), if_neg (Nat.ne_of_lt x₂.isLt)] at hg - let x₁m : Fin m := ⟨↑x₁, calc ↑x₁ - _ < nat_p := x₁.isLt - _ < m := hnat_p_lt_m⟩ - let x₂m : Fin m := ⟨↑x₂, calc ↑x₂ - _ < nat_p := x₂.isLt - _ < m := hnat_p_lt_m⟩ - by_cases hx₁ : x₁m = fin_t - · by_cases hx₂ : x₂m = fin_t - · rw [Fin.ext_iff] at hx₁ hx₂ ⊢ - rw [show x₁.1 = x₁m.1 from rfl, show x₂.1 = x₂m.1 from rfl, hx₁, hx₂] - · rw [if_pos hx₁, if_neg hx₂, ← Fin.ext_iff] at hg - have := hf_inj hg - rw [Fin.ext_iff] at this - exact absurd this.symm (Nat.ne_of_lt x₂.isLt) - · by_cases hx₂ : x₂m = fin_t - · rw [if_neg hx₁, if_pos hx₂, ← Fin.ext_iff] at hg - have := hf_inj hg - rw [Fin.ext_iff] at this - exact absurd this (Nat.ne_of_lt x₁.isLt) - · rw [if_neg hx₁, if_neg hx₂, ← Fin.ext_iff] at hg - have := hf_inj hg - simp only [Fin.mk.injEq] at this - exact Fin.ext_iff.mpr this + 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 - have ng_surj : ¬ Function.Surjective g := ih nat_p (calc nat_p - _ < m := hnat_p_lt_m - _ ≤ n := Nat.lt_succ.mp hm) g hg_inj - -- We have shown `g` isn't surjective. This is another way of saying that. - have ⟨a, ha⟩ : ∃ a, a ∉ Set.range g := by - unfold Function.Surjective at ng_surj - unfold Set.range - simp only [not_forall, not_exists] at ng_surj - have ⟨a, ha₁⟩ := ng_surj - simp only [Fin.mk.injEq] at ha₁ - refine ⟨a, ?_⟩ - intro ha₂ - simp only [Fin.mk.injEq, Set.mem_setOf_eq] at ha₂ - have ⟨y, hy⟩ := ha₂ - exact absurd hy (ha₁ y) + 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 - -- By construction, if `g` isn't surjective then neither is `f'`. - have hf'a : ↑a ∉ Set.range f' := by + -- 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 ?_) - -- It suffices to prove that `f'` and `g` agree on all values found in - -- `g`'s domain. The only input that complicates things is `p`, which is - -- found in the domains of `f'` and `f`. So long as we can prove - -- `f' p ≠ a`, then we can be sure `a` appears nowhere in `ran f'`. - suffices ∀ x : Fin m, (ht : x < fin_p) → f' x = g ⟨x, ht⟩ by - unfold Set.range - simp only [Set.mem_setOf_eq, not_exists] + 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 - intro x - by_cases hp : x = fin_p - · intro nx - rw [if_pos hp, Fin.ext_iff] at nx - simp only [ - Fin.coe_ofNat_eq_mod, - Fin.coe_eq_castSucc, - Fin.coe_castSucc - ] at nx - rw [Nat.mod_succ_eq_iff_lt.mpr (show n < n + 1 by simp)] at nx - exact absurd nx (Nat.ne_of_lt a.isLt).symm - - · show f' x ≠ ↑↑a - rw [show ¬x = fin_p ↔ x ≠ fin_p from Iff.rfl, ← Fin.val_ne_iff] at hp - - -- Apply our `suffice` hypothesis. - have hx_lt_fin_p : x < fin_p := by - refine Or.elim (Nat.lt_or_eq_of_lt $ calc ↑x - _ < m := x.isLt - _ = nat_p + 1 := hnat_p) id ?_ - intro hxp - exact absurd hxp hp - rw [this x hx_lt_fin_p] - - have ha₁ : ¬∃ y, g y = a := ha - simp only [not_exists] at ha₁ - have ha₂ : g ⟨↑x, _⟩ ≠ a := - ha₁ ⟨↑x, by rwa [Fin.lt_iff_val_lt_val] at hx_lt_fin_p⟩ - norm_cast at ha₂ ⊢ - intro nx - exact absurd (Fin.castSucc_injective n nx) ha₂ - - intro t ht - rw [Fin.ext_iff] - simp only [Fin.coe_ofNat_eq_mod] - generalize ( - if t = fin_p then ↑n - else if t = fin_t then f fin_p - else f t - ) = y - exact (Nat.mod_succ_eq_iff_lt.mpr y.isLt).symm - - -- Likewise, if `f'` isn't surjective then neither is `f`. - have hfa : ↑a ∉ Set.range f := by - suffices Set.range f = Set.range f' by rw [this]; exact hf'a - unfold Set.range - ext x - apply Iff.intro - · intro ⟨y, hy⟩ - simp only [Set.mem_setOf_eq] - by_cases hx₁ : x = n - · refine ⟨fin_p, ?_⟩ + 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 hx₁.symm - · by_cases hx₂ : x = ⟨f fin_p, (f fin_p).isLt⟩ - · refine ⟨fin_t, ?_⟩ - by_cases ht : fin_t = fin_p - · rw [if_pos ht, hx₂] - rw [ht] at hfin_t - exact hfin_t.symm - · rw [if_neg ht, if_pos rfl, hx₂] - · refine ⟨y, ?_⟩ - have hy₁ : y ≠ fin_p := by - by_contra ny - rw [ny] at hy - exact absurd hy.symm hx₂ - have hy₂ : y ≠ fin_t := by - by_contra ny - rw [ny, hfin_t] at hy - exact absurd hy.symm hx₁ - rw [if_neg hy₁, if_neg hy₂] - exact hy - · intro ⟨y, hy⟩ - dsimp only at hy - by_cases hy₁ : y = fin_p - · rw [if_pos hy₁] at hy - have := hf_surj ⟨n, show n < n + 1 by simp⟩ - rwa [← hy] - · rw [if_neg hy₁] at hy - by_cases hy₂ : y = fin_t - · rw [if_pos hy₂] at hy - exact ⟨fin_p, hy⟩ - · rw [if_neg hy₂] at hy - exact ⟨y, hy⟩ + 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₂] - simp only [Fin.coe_eq_castSucc, Set.mem_setOf_eq] at hfa - exact absurd (hf_surj $ Fin.castSucc a) hfa - -theorem pigeonhole_principle (m n : ℕ) (h : m < n) - : ∀ f : Fin m → Fin n, ¬ Function.Bijective f := by - intro f nf - have := pigeonhole_principle_aux n m h f nf.left - exact absurd nf.right this +/-- +No natural number is equinumerous to a proper subset of itself. +-/ +theorem pigeonhole_principle {n : ℕ} + : ∀ M, M ⊂ Set.Iio n → ∀ f, ¬ Set.BijOn f M (Set.Iio n) := by + intro M hM f nf + have := pigeonhole_principle_aux n M hM f ⟨nf.left, nf.right.left⟩ + exact absurd nf.right.right this /-- #### Corollary 6C No finite set is equinumerous to a proper subset of itself. -/ -theorem corollary_6c (S S' : Finset α) (hS : S' ⊂ S) - : ∀ f : S → S', ¬ Function.Bijective f := by - sorry +theorem corollary_6c [DecidableEq α] [Nonempty α] {S S' : Finset α} (h : S' ⊂ S) + : ∀ f, ¬ Set.BijOn f S.toSet S'.toSet := by + have ⟨T, hT₁, hT₂⟩ : ∃ T, Disjoint S' T ∧ S = S' ∪ T := by + refine ⟨S \ S', ?_, ?_⟩ + · intro X hX₁ hX₂ + show ∀ t, t ∈ X → t ∈ ⊥ + intro t ht + have ht₂ := hX₂ ht + simp only [Finset.mem_sdiff] at ht₂ + exact absurd (hX₁ ht) ht₂.right + · simp only [ + Finset.union_sdiff_self_eq_union, + Finset.right_eq_union_iff_subset + ] + exact subset_of_ssubset h + + -- `hF : S' ∪ T ≈ S`. + -- `hG : S ≈ n`. + -- `hH : S' ∪ T ≈ n`. + have ⟨F, hF⟩ := Set.equinumerous_refl S.toSet + conv at hF => arg 2; rw [hT₂] + have ⟨n, G, hG⟩ := Set.finite_iff_equinumerous_nat.mp (Finset.finite_toSet S) + have ⟨H, hH⟩ := Set.equinumerous_trans hF hG + + -- Restrict `H` to `S'` to yield a bijection between `S'` and `m < 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 $ Finset.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 := Finset.mem_union_right S' ha₁ + have hc₂ : x ∈ S' ∪ T := Finset.mem_union_left T hx + rw [hH.right.left hc₁ hc₂ ha₂] at ha₁ + + have hx₁ : {x} ⊆ S' := Finset.singleton_subset_iff.mpr hx + have hx₂ : {x} ⊆ T := Finset.singleton_subset_iff.mpr ha₁ + have hx₃ := hT₁ hx₁ hx₂ + simp only [ + Finset.bot_eq_empty, + Finset.le_eq_subset, + Finset.singleton_subset_iff, + Finset.not_mem_empty + ] at hx₃ + · -- `Set.InjOn H S'` + intro x₁ hx₁ x₂ hx₂ h + have hc₁ : x₁ ∈ S' ∪ T := Finset.mem_union_left T hx₁ + have hc₂ : x₂ ∈ S' ∪ T := Finset.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 [Finset.mem_coe, Set.mem_setOf_eq] + dsimp only at hr + have := hH.right.right hr.left + simp only [ + Finset.coe_union, + Set.mem_image, + Set.mem_union, + Finset.mem_coe + ] 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 f nf + have ⟨f₁, hf₁⟩ : ∃ f₁ : α → ℕ, Set.BijOn f₁ S R := + Set.equinumerous_trans nf hR + have ⟨f₂, hf₂⟩ : ∃ f₃ : ℕ → ℕ, Set.BijOn f₃ R (Set.Iio n) := by + have ⟨k, hk₁⟩ := Set.equinumerous_symm hf₁ + exact Set.equinumerous_trans hk₁ hG + + refine absurd hf₂ (pigeonhole_principle R ?_ f₂) + 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₁⟩ : Finset.Nonempty T := by + rw [hT₂, Finset.ssubset_def] at h + have : ¬ ∀ x, x ∈ S' ∪ T → x ∈ S' := h.right + simp only [Finset.mem_union, not_forall, exists_prop] at this + have ⟨x, hx⟩ := this + apply Or.elim hx.left + · intro nx + exact absurd nx hx.right + · intro hx + exact ⟨x, hx⟩ + have ht₂ : H t ∈ Set.Iio n := hH.left (Finset.mem_union_right S' ht₁) + have ht₃ : H t ∈ R := nr (H t) ht₂ + exact absurd ⟨t, ht₁, rfl⟩ ht₃.right /-- #### Corollary 6D (a) diff --git a/Common/Real/Floor.lean b/Common/Real/Floor.lean index e0356e1..162a67a 100644 --- a/Common/Real/Floor.lean +++ b/Common/Real/Floor.lean @@ -99,7 +99,7 @@ end Hermite open BigOperators -/-- ### Hermite's Identity +/-- #### Hermite's Identity The following decomposes the floor of a multiplication into a sum of floors. -/ diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index dcb5eff..ed7c765 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -1,6 +1,7 @@ import Common.Logic.Basic import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Prod +import Mathlib.Tactic.LibrarySearch /-! # Common.Set.Basic @@ -68,11 +69,15 @@ theorem pair_eq_singleton_mem_imp_eq_all {x y z : α} /-! ## Subsets -/ /-- -Every `Set` is a subset of itself. +There exists no proper subset of `∅`. -/ -theorem subset_self (S : Set α) : S ⊆ S := by - intro _ hs - exact hs +theorem ssubset_empty_iff_false (S : Set α) + : S ⊂ ∅ ↔ False := by + apply Iff.intro + · intro h + rw [ssubset_iff_subset_ne, subset_empty_iff] at h + exact absurd h.left h.right + · simp only [IsEmpty.forall_iff] /-- If `Set` `A` is a subset of `Set` `B`, then `A ∪ B = B`. @@ -116,7 +121,7 @@ theorem mem_mem_imp_pair_subset {x y : α} Every `Set` is a member of its own powerset. -/ theorem self_mem_powerset_self {A : Set α} - : A ∈ 𝒫 A := subset_self A + : A ∈ 𝒫 A := fun _ => mem_preimage.mp /-! ## Cartesian Product -/ @@ -156,6 +161,20 @@ theorem prod_nonempty_nonempty_imp_nonempty_prod {A : Set α} {B : Set β} /-! ## Difference -/ +/-- +For any sets `A ⊂ B`, if `x ∈ A` then `A - {x} ⊂ B - {x}`. +-/ +theorem diff_ssubset_diff_left {A B : Set α} (h : A ⊂ B) + : x ∈ A → A \ {x} ⊂ B \ {x} := by + intro hx + rw [Set.ssubset_def] + apply And.intro + · exact diff_subset_diff_left (subset_of_ssubset h) + · by_contra nh + have : {x} ⊆ A := singleton_subset_iff.mpr hx + rw [diff_subset_iff, union_diff_cancel this] at nh + exact LT.lt.false (Set.ssubset_of_ssubset_of_subset h nh) + /-- For any set `A`, the difference between the sample space and `A` is the complement of `A`. diff --git a/Common/Set/Finite.lean b/Common/Set/Finite.lean new file mode 100644 index 0000000..876d216 --- /dev/null +++ b/Common/Set/Finite.lean @@ -0,0 +1,45 @@ +import Mathlib.Data.Finset.Card +import Mathlib.Data.Set.Finite + +/-! # Common.Set.Finite + +Additional theorems around finite sets. +-/ + +namespace Set + +/-- +For any set `A`, `A ≈ A`. +-/ +theorem equinumerous_refl (A : Set α) + : ∃ F, Set.BijOn F A A := by + refine ⟨fun x => x, ?_⟩ + unfold Set.BijOn Set.MapsTo Set.InjOn Set.SurjOn + simp only [imp_self, implies_true, Set.image_id', true_and] + exact Eq.subset rfl + +/-- +For any sets `A` and `B`, if `A ≈ B`. then `B ≈ A`. +-/ +theorem equinumerous_symm [Nonempty α] {A : Set α} {B : Set β} + {F : α → β} (hF : Set.BijOn F A B) + : ∃ G, Set.BijOn G B A := by + refine ⟨Function.invFunOn F A, ?_⟩ + exact (Set.bijOn_comm $ Set.BijOn.invOn_invFunOn hF).mpr hF + +/-- +For any sets `A`, `B`, and `C`, if `A ≈ B` and `B ≈ C`, then `A ≈ C`. +-/ +theorem equinumerous_trans {A : Set α} {B : Set β} {C : Set γ} + {F : α → β} (hF : Set.BijOn F A B) + {G : β → γ} (hG : Set.BijOn G B C) + : ∃ H, Set.BijOn H A C := by + exact ⟨G ∘ F, Set.BijOn.comp hG hF⟩ + +/-- +A set is finite if and only if it is equinumerous to a natural number. +-/ +axiom finite_iff_equinumerous_nat {α : Type _} {S : Set α} + : Set.Finite S ↔ ∃ n : ℕ, ∃ f, Set.BijOn f S (Set.Iio n) + +end Set \ No newline at end of file