From 2a85d526d75e8177f9c77a2d95d68f893b6ec44c Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sun, 17 Sep 2023 12:07:24 -0600 Subject: [PATCH] Enderton (set). Finish equinumerosity theorems. --- Bookshelf/Enderton/Set.tex | 26 +- Bookshelf/Enderton/Set/Chapter_6.lean | 388 +++++++++++++++++++++----- Common/Set.lean | 2 + Common/Set/Basic.lean | 18 ++ Common/Set/Equinumerous.lean | 86 ++++++ Common/Set/Finite.lean | 45 --- Common/Set/Intervals.lean | 25 ++ 7 files changed, 465 insertions(+), 125 deletions(-) create mode 100644 Common/Set/Equinumerous.lean delete mode 100644 Common/Set/Finite.lean create mode 100644 Common/Set/Intervals.lean diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 8f46ca8..a18d105 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -150,6 +150,9 @@ \lean*{Mathlib/Init/Function} {Function.Bijective} + \lean{Mathlib/Data/Set/Function} + {Set.BijOn} + \lean{Mathlib/Logic/Equiv/Defs} {Equiv} @@ -8973,7 +8976,7 @@ Hence no finite set is equinumerous to a proper subset of itself. \end{proof} -\subsection{\pending{Corollary 6D}}% +\subsection{\verified{Corollary 6D}}% \hyperlabel{sub:corollary-6d} \begin{corollary}[6D] @@ -8984,6 +8987,12 @@ \end{enumerate} \end{corollary} + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.corollary\_6d\_a} + + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.corollary\_6d\_b} + \begin{proof} \paragraph{(a)}% @@ -9034,13 +9043,16 @@ \end{proof} -\subsection{\pending{Corollary 6E}}% +\subsection{\verified{Corollary 6E}}% \hyperlabel{sub:corollary-6e} \begin{corollary}[6E] Any finite set is equinumerous to a unique natural number. \end{corollary} + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.corollary\_6e} + \begin{proof} Let $S$ be a \nameref{ref:finite-set}. By definition $S$ is equinumerous to a natural number $n$. @@ -9057,7 +9069,7 @@ number. \end{proof} -\subsection{\pending{Lemma 6F}}% +\subsection{\verified{Lemma 6F}}% \hyperlabel{sub:lemma-6f} \begin{lemma}[6F] @@ -9065,6 +9077,9 @@ some $m$ less than $n$. \end{lemma} + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.lemma\_6f} + \begin{proof} Let @@ -9132,13 +9147,16 @@ \end{proof} -\subsection{\pending{Corollary 6G}}% +\subsection{\verified{Corollary 6G}}% \hyperlabel{sub:corollary-6g} \begin{corollary}[6G] Any subset of a finite set is finite. \end{corollary} + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.corollary\_6g} + \begin{proof} Let $S$ be a \nameref{ref:finite-set} and $S' \subseteq S$. Clearly, if $S' = S$, then $S'$ is finite. diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean index 609d2bc..e87c4fa 100644 --- a/Bookshelf/Enderton/Set/Chapter_6.lean +++ b/Bookshelf/Enderton/Set/Chapter_6.lean @@ -1,7 +1,9 @@ +import Bookshelf.Enderton.Set.Chapter_4 import Common.Logic.Basic import Common.Nat.Basic import Common.Set.Basic -import Common.Set.Finite +import Common.Set.Equinumerous +import Common.Set.Intervals import Mathlib.Data.Finset.Card import Mathlib.Data.Set.Finite import Mathlib.Tactic.LibrarySearch @@ -23,7 +25,8 @@ namespace Enderton.Set.Chapter_6 No set is equinumerous to its powerset. -/ theorem theorem_6b (A : Set α) - : ∀ f, ¬ Set.BijOn f A (𝒫 A) := by + : A ≉ 𝒫 A := by + rw [Set.not_equinumerous_def] intro f hf unfold Set.BijOn at hf let φ := { a ∈ A | a ∉ f a } @@ -287,82 +290,71 @@ lemma pigeonhole_principle_aux (n : ℕ) 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 + : ∀ {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' : 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 +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 ⟨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 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 `m < n`. + -- 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 $ Finset.mem_union_left T 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 := Finset.mem_union_right S' ha₁ - have hc₂ : x ∈ S' ∪ T := Finset.mem_union_left T hx + 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' := Finset.singleton_subset_iff.mpr hx - have hx₂ : {x} ⊆ T := Finset.singleton_subset_iff.mpr ha₁ - have hx₃ := hT₁ hx₁ hx₂ + 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 [ - Finset.bot_eq_empty, - Finset.le_eq_subset, - Finset.singleton_subset_iff, - Finset.not_mem_empty - ] at hx₃ + 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 := Finset.mem_union_left T hx₁ - have hc₂ : x₂ ∈ S' ∪ T := Finset.mem_union_left T hx₂ + 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 [Finset.mem_coe, Set.mem_setOf_eq] + simp only [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 + simp only [Set.mem_image, Set.mem_union] at this have ⟨x, hx⟩ := this apply Or.elim hx.left · intro hx' @@ -372,15 +364,14 @@ theorem corollary_6c [DecidableEq α] [Nonempty α] {S S' : Finset α} (h : S' 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 + + 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 R ?_ f₂) + refine absurd hf₂ (pigeonhole_principle ?_) show R ⊂ Set.Iio n apply And.intro · show ∀ r, r ∈ R → r ∈ Set.Iio n @@ -388,17 +379,8 @@ theorem corollary_6c [DecidableEq α] [Nonempty α] {S S' : Finset α} (h : S' 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 ⟨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 @@ -406,9 +388,12 @@ theorem corollary_6c [DecidableEq α] [Nonempty α] {S S' : Finset α} (h : S' Any set equinumerous to a proper subset of itself is infinite. -/ -theorem corollary_6d_a (S S' : Set α) (hS : S' ⊂ S) (hf : S' ≃ S) +theorem corollary_6d_a [DecidableEq α] [Nonempty α] + {S S' : Set α} (hS : S' ⊂ S) (hf : S ≈ S') : Set.Infinite S := by - sorry + by_contra nS + simp only [Set.not_infinite] at nS + exact absurd hf (corollary_6c nS hS) /-- #### Corollary 6D (b) @@ -416,28 +401,279 @@ The set `ω` is infinite. -/ theorem corollary_6d_b : Set.Infinite (@Set.univ ℕ) := by - sorry + 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 (S : Set α) (hn : S ≃ Fin n) (hm : S ≃ Fin m) - : m = n := by - sorry +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 : ℕ} (hC : C ⊂ Finset.range n) - : ∃ m : ℕ, m < n ∧ ∃ f : C → Fin m, Function.Bijective f := by - sorry +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⟩ -theorem corollary_6g (S S' : Set α) (hS : Finite S) (hS' : S' ⊆ S) - : Finite S' := by - sorry + 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 diff --git a/Common/Set.lean b/Common/Set.lean index 44465b9..ef5f266 100644 --- a/Common/Set.lean +++ b/Common/Set.lean @@ -1,2 +1,4 @@ import Common.Set.Basic +import Common.Set.Equinumerous +import Common.Set.Intervals import Common.Set.Peano \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index ed7c765..51d3d92 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -175,6 +175,24 @@ theorem diff_ssubset_diff_left {A B : Set α} (h : A ⊂ B) rw [diff_subset_iff, union_diff_cancel this] at nh exact LT.lt.false (Set.ssubset_of_ssubset_of_subset h nh) +/-- +For any sets `A ⊂ B`, `B \ A` is nonempty. +-/ +theorem diff_ssubset_nonempty {A B : Set α} (h : A ⊂ B) + : Set.Nonempty (B \ A) := by + have : B = A ∪ (B \ A) := by + simp only [Set.union_diff_self] + exact (Set.left_subset_union_eq_self (subset_of_ssubset h)).symm + rw [this, Set.ssubset_def] at h + have : ¬ ∀ x, x ∈ A ∪ (B \ A) → x ∈ A := h.right + simp only [Set.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⟩ + /-- For any set `A`, the difference between the sample space and `A` is the complement of `A`. diff --git a/Common/Set/Equinumerous.lean b/Common/Set/Equinumerous.lean new file mode 100644 index 0000000..6351a0f --- /dev/null +++ b/Common/Set/Equinumerous.lean @@ -0,0 +1,86 @@ +import Mathlib.Data.Finset.Card +import Mathlib.Data.Set.Finite + +/-! # Common.Set.Finite + +Additional theorems around finite sets. +-/ + +namespace Set + +/-- +A set `A` is equinumerous to a set `B` (written `A ≈ B`) if and only if there is +a one-to-one function from `A` onto `B`. +-/ +def Equinumerous (A : Set α) (B : Set β) : Prop := ∃ F, Set.BijOn F A B + +infix:50 " ≈ " => Equinumerous + +theorem equinumerous_def (A : Set α) (B : Set β) + : A ≈ B ↔ ∃ F, Set.BijOn F A B := Iff.rfl + +/-- +For any set `A`, `A ≈ A`. +-/ +theorem equinumerous_refl (A : Set α) + : 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 β} + (h : A ≈ B) : B ≈ A := by + have ⟨F, hF⟩ := h + 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 γ} + (h₁ : A ≈ B) (h₂ : B ≈ C) + : ∃ H, Set.BijOn H A C := by + have ⟨F, hF⟩ := h₁ + have ⟨G, hG⟩ := h₂ + exact ⟨G ∘ F, Set.BijOn.comp hG hF⟩ + +/-- +If two sets are equal, they are trivially equinumerous. +-/ +theorem eq_imp_equinumerous {A B : Set α} (h : A = B) + : A ≈ B := by + have := equinumerous_refl A + conv at this => right; rw [h] + exact this + +/-- +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 : ℕ, S ≈ Set.Iio n + +/-- +A set `A` is not equinumerous to a set `B` (written `A ≉ B`) if and only if +there is no one-to-one function from `A` onto `B`. +-/ +def NotEquinumerous (A : Set α) (B : Set β) : Prop := ¬ Equinumerous A B + +infix:50 " ≉ " => NotEquinumerous + +@[simp] +theorem not_equinumerous_def : A ≉ B ↔ ∀ F, ¬ Set.BijOn F A B := by + apply Iff.intro + · intro h + unfold NotEquinumerous Equinumerous at h + simp only [not_exists] at h + exact h + · intro h + unfold NotEquinumerous Equinumerous + simp only [not_exists] + exact h + +end Set \ No newline at end of file diff --git a/Common/Set/Finite.lean b/Common/Set/Finite.lean deleted file mode 100644 index 876d216..0000000 --- a/Common/Set/Finite.lean +++ /dev/null @@ -1,45 +0,0 @@ -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 diff --git a/Common/Set/Intervals.lean b/Common/Set/Intervals.lean new file mode 100644 index 0000000..433e288 --- /dev/null +++ b/Common/Set/Intervals.lean @@ -0,0 +1,25 @@ +import Common.Logic.Basic +import Mathlib.Data.Set.Intervals.Basic + +namespace Set + +/-! # Common.Set.Intervals + +Additional theorems around intervals. +-/ + +theorem Iio_nat_lt_ssubset {m n : ℕ} (h : m < n) + : Iio m ⊂ Iio n := by + rw [ssubset_def] + apply And.intro + · unfold Iio + simp only [setOf_subset_setOf] + intro x hx + calc x + _ < m := hx + _ < n := h + · show ¬ ∀ x, x < n → x < m + simp only [not_forall, not_lt, exists_prop] + exact ⟨m, h, by simp⟩ + +end Set \ No newline at end of file