From 1eff704803255d63179aca8b039053f984cf9b0f Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 9 Aug 2023 12:59:23 -0600 Subject: [PATCH] Start fixing up unverified. --- Bookshelf/Apostol/Chapter_I_03.lean | 1 + Bookshelf/Enderton/Set.tex | 53 ++++++++--- Bookshelf/Enderton/Set/Chapter_2.lean | 124 ++++++++++++++++++++++---- 3 files changed, 148 insertions(+), 30 deletions(-) diff --git a/Bookshelf/Apostol/Chapter_I_03.lean b/Bookshelf/Apostol/Chapter_I_03.lean index 0c7da3e..c5f6512 100644 --- a/Bookshelf/Apostol/Chapter_I_03.lean +++ b/Bookshelf/Apostol/Chapter_I_03.lean @@ -9,6 +9,7 @@ A Set of Axioms for the Real-Number System namespace Apostol.Chapter_I_03 #check Archimedean + #check Real.exists_isLUB /-! ## The least-upper-bound axiom (completeness axiom) -/ diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index e28c5ec..eb286a6 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -1165,7 +1165,7 @@ \end{proof} -\subsection{\pending{Monotonicity}}% +\subsection{\verified{Monotonicity}}% \hyperlabel{sub:monotonicity} For any sets $A$, $B$, and $C$, @@ -1175,11 +1175,23 @@ A \subseteq B & \Rightarrow \bigcup A \subseteq \bigcup B \end{align*} - \lean{Mathlib/Data/Set/Basic}{Set.union\_subset\_union\_left} + \lean{Mathlib/Data/Set/Basic} + {Set.union\_subset\_union\_left} - \lean{Mathlib/Data/Set/Basic}{Set.inter\_subset\_inter\_left} + \code{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.monotonicity\_i} - \lean{Mathlib/Data/Set/Lattice}{Set.sUnion\_mono} + \lean{Mathlib/Data/Set/Basic} + {Set.inter\_subset\_inter\_left} + + \code{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.monotonicity\_ii} + + \lean{Mathlib/Data/Set/Lattice} + {Set.sUnion\_mono} + + \code{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.monotonicity\_iii} \begin{proof} @@ -1236,7 +1248,7 @@ \end{proof} -\subsection{\pending{Anti-monotonicity}}% +\subsection{\verified{Anti-monotonicity}}% \hyperlabel{sub:anti-monotonicity} For any sets $A$, $B$, and $C$, @@ -1245,9 +1257,17 @@ \emptyset \neq A \subseteq B & \Rightarrow \bigcap B \subseteq \bigcap A. \end{align*} - \lean{Mathlib/Data/Set/Basic}{Set.diff\_subset\_diff\_right} + \lean{Mathlib/Data/Set/Basic} + {Set.diff\_subset\_diff\_right} - \lean{Mathlib/Data/Set/Lattice}{Set.sInter\_subset\_sInter} + \code{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.anti\_monotonicity\_i} + + \lean{Mathlib/Data/Set/Lattice} + {Set.sInter\_subset\_sInter} + + \code{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.anti\_monotonicity\_ii} \begin{proof} @@ -1404,14 +1424,18 @@ \end{proof} -\subsection{\pending{% +\subsection{\verified{% \texorpdfstring{$\cap$/$-$}{Intersection/Difference} Associativity}}% \hyperlabel{sub:intersection-difference-associativity} Let $A$, $B$, and $C$ be sets. Then $A \cap (B - C) = (A \cap B) - C$. - \lean*{Mathlib/Data/Set/Basic}{Set.inter\_diff\_assoc} + \lean*{Mathlib/Data/Set/Basic} + {Set.inter\_diff\_assoc} + + \code{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.inter\_diff\_assoc} \begin{proof} Let $A$, $B$, and $C$ be sets. @@ -2626,7 +2650,7 @@ This concludes our proof. \end{proof} -\subsection{\pending{Corollary 3C}}% +\subsection{\unverified{Corollary 3C}}% \hyperlabel{sub:corollary-3c} \begin{theorem}[3C] @@ -2634,13 +2658,14 @@ pairs $\pair{x, y}$ with $x \in A$ and $y \in B$. \end{theorem} + \begin{note} + The below Lean proof is a definition (i.e. an axiom). + It does not prove such a set's existence from first principles. + \end{note} + \lean{Mathlib/SetTheory/ZFC/Basic}{Set.prod} \begin{proof} - \begin{note} - The above Lean proof is a definition (i.e. an axiom). - It does not prove such a set's existence from first principles. - \end{note} Define $C = A \cup B$. Then for all $x \in A$ and for all $y \in B$, $x$ and $y$ are both in $C$. By \nameref{sub:lemma-3b}, it follows that diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean index c604ed9..07e949e 100644 --- a/Bookshelf/Enderton/Set/Chapter_2.lean +++ b/Bookshelf/Enderton/Set/Chapter_2.lean @@ -18,8 +18,6 @@ A ∩ B = B ∩ A ``` -/ -#check Set.union_comm - theorem commutative_law_i (A B : Set α) : A ∪ B = B ∪ A := calc A ∪ B _ = { x | x ∈ A ∨ x ∈ B } := rfl @@ -28,7 +26,7 @@ theorem commutative_law_i (A B : Set α) exact or_comm _ = B ∪ A := rfl -#check Set.inter_comm +#check Set.union_comm theorem commutative_law_ii (A B : Set α) : A ∩ B = B ∩ A := calc A ∩ B @@ -38,6 +36,8 @@ theorem commutative_law_ii (A B : Set α) exact and_comm _ = B ∩ A := rfl +#check Set.inter_comm + /-! #### Associative Laws For any sets `A`, `B`, and `C`, @@ -47,8 +47,6 @@ A ∩ (B ∩ C) = (A ∩ B) ∩ C ``` -/ -#check Set.union_assoc - theorem associative_law_i (A B C : Set α) : A ∪ (B ∪ C) = (A ∪ B) ∪ C := calc A ∪ (B ∪ C) _ = { x | x ∈ A ∨ x ∈ B ∪ C } := rfl @@ -60,7 +58,7 @@ theorem associative_law_i (A B C : Set α) _ = { x | x ∈ A ∪ B ∨ x ∈ C } := rfl _ = (A ∪ B) ∪ C := rfl -#check Set.inter_assoc +#check Set.union_assoc theorem associative_law_ii (A B C : Set α) : A ∩ (B ∩ C) = (A ∩ B) ∩ C := calc A ∩ (B ∩ C) @@ -73,6 +71,8 @@ theorem associative_law_ii (A B C : Set α) _ = { x | x ∈ A ∩ B ∧ x ∈ C } := rfl _ = (A ∩ B) ∩ C := rfl +#check Set.inter_assoc + /-! #### Distributive Laws For any sets `A`, `B`, and `C`, @@ -82,8 +82,6 @@ A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C) ``` -/ -#check Set.inter_distrib_left - theorem distributive_law_i (A B C : Set α) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := calc A ∩ (B ∪ C) _ = { x | x ∈ A ∧ x ∈ B ∪ C } := rfl @@ -94,7 +92,7 @@ theorem distributive_law_i (A B C : Set α) _ = { x | x ∈ A ∩ B ∨ x ∈ A ∩ C } := rfl _ = (A ∩ B) ∪ (A ∩ C) := rfl -#check Set.union_distrib_left +#check Set.inter_distrib_left theorem distributive_law_ii (A B C : Set α) : A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C) := calc A ∪ (B ∩ C) @@ -106,6 +104,8 @@ theorem distributive_law_ii (A B C : Set α) _ = { x | x ∈ A ∪ B ∧ x ∈ A ∪ C } := rfl _ = (A ∪ B) ∩ (A ∪ C) := rfl +#check Set.union_distrib_left + /-! #### De Morgan's Laws For any sets `A`, `B`, and `C`, @@ -115,8 +115,6 @@ C - (A ∩ B) = (C - A) ∪ (C - B) ``` -/ -#check Set.diff_inter_diff - theorem de_morgans_law_i (A B C : Set α) : C \ (A ∪ B) = (C \ A) ∩ (C \ B) := calc C \ (A ∪ B) _ = { x | x ∈ C ∧ x ∉ A ∪ B } := rfl @@ -131,7 +129,7 @@ theorem de_morgans_law_i (A B C : Set α) _ = { x | x ∈ C \ A ∧ x ∈ C \ B } := rfl _ = (C \ A) ∩ (C \ B) := rfl -#check Set.diff_inter +#check Set.diff_inter_diff theorem de_morgans_law_ii (A B C : Set α) : C \ (A ∩ B) = (C \ A) ∪ (C \ B) := calc C \ (A ∩ B) @@ -147,6 +145,8 @@ theorem de_morgans_law_ii (A B C : Set α) _ = { x | x ∈ C \ A ∨ x ∈ C \ B } := rfl _ = (C \ A) ∪ (C \ B) := rfl +#check Set.diff_inter + /-! #### Identities Involving ∅ For any set `A`, @@ -157,8 +157,6 @@ A ∩ (C - A) = ∅ ``` -/ -#check Set.union_empty - theorem emptyset_identity_i (A : Set α) : A ∪ ∅ = A := calc A ∪ ∅ _ = { x | x ∈ A ∨ x ∈ ∅ } := rfl @@ -166,7 +164,7 @@ theorem emptyset_identity_i (A : Set α) _ = { x | x ∈ A } := by simp _ = A := rfl -#check Set.inter_empty +#check Set.union_empty theorem emptyset_identity_ii (A : Set α) : A ∩ ∅ = ∅ := calc A ∩ ∅ @@ -175,7 +173,7 @@ theorem emptyset_identity_ii (A : Set α) _ = { x | False } := by simp _ = ∅ := rfl -#check Set.inter_diff_self +#check Set.inter_empty theorem emptyset_identity_iii (A C : Set α) : A ∩ (C \ A) = ∅ := calc A ∩ (C \ A) @@ -185,6 +183,100 @@ theorem emptyset_identity_iii (A C : Set α) _ = { x | False } := by simp _ = ∅ := rfl +#check Set.inter_diff_self + +/-! #### Monotonicity + +For any sets `A`, `B`, and `C`, +``` +A ⊆ B ⇒ A ∪ C ⊆ B ∪ C +A ⊆ B ⇒ A ∩ C ⊆ B ∩ C +A ⊆ B ⇒ ⋃ A ⊆ ⋃ B +``` +-/ + +theorem monotonicity_i (A B C : Set α) (h : A ⊆ B) + : A ∪ C ⊆ B ∪ C := by + show ∀ x, x ∈ A ∪ C → x ∈ B ∪ C + intro x hx + apply Or.elim hx + · intro hA + have := h hA + left + exact this + · intro hC + right + exact hC + +#check Set.union_subset_union_left + +theorem monotonicity_ii (A B C : Set α) (h : A ⊆ B) + : A ∩ C ⊆ B ∩ C := by + show ∀ x, x ∈ A ∩ C → x ∈ B ∩ C + intro x hx + have := h hx.left + exact ⟨this, hx.right⟩ + +#check Set.inter_subset_inter_left + +theorem monotonicity_iii (A B : Set (Set α)) (h : A ⊆ B) + : ⋃₀ A ⊆ ⋃₀ B := by + show ∀ x, x ∈ ⋃₀ A → x ∈ ⋃₀ B + intro x hx + have ⟨b, hb⟩ := hx + have := h hb.left + exact ⟨b, this, hb.right⟩ + +#check Set.sUnion_mono + +/-! #### Anti-monotonicity + +For any sets `A`, `B`, and `C`, +``` +A ⊆ B ⇒ C - B ⊆ C - A +∅ ≠ A ⊆ B ⇒ ⋂ B ⊆ ⋂ A +``` +-/ + +theorem anti_monotonicity_i (A B C : Set α) (h : A ⊆ B) + : C \ B ⊆ C \ A := by + show ∀ x, x ∈ C \ B → x ∈ C \ A + intro x hx + have : x ∉ A := by + by_contra nh + have := h nh + exact absurd this hx.right + exact ⟨hx.left, this⟩ + +#check Set.diff_subset_diff_right + +theorem anti_monotonicity_ii (A B : Set (Set α)) (h : A ⊆ B) + : ⋂₀ B ⊆ ⋂₀ A := by + show ∀ x, x ∈ ⋂₀ B → x ∈ ⋂₀ A + intro x hx + have : ∀ b, b ∈ B → x ∈ b := hx + show ∀ a, a ∈ A → x ∈ a + intro a ha + exact this a (h ha) + +#check Set.sInter_subset_sInter + +/-- #### ∩/- Associativity + +Let `A`, `B`, and `C` be sets. Then `A ∩ (B - C) = (A ∩ B) - C`. +-/ +theorem inter_diff_assoc (A B C : Set α) + : A ∩ (B \ C) = (A ∩ B) \ C := calc A ∩ (B \ C) + _ = { x | x ∈ A ∧ x ∈ (B \ C) } := rfl + _ = { x | x ∈ A ∧ (x ∈ B ∧ x ∉ C) } := rfl + _ = { x | (x ∈ A ∧ x ∈ B) ∧ x ∉ C } := by + ext _ + sorry + _ = { x | x ∈ A ∩ B ∧ x ∉ C } := rfl + _ = (A ∩ B) \ C := rfl + +#check Set.inter_diff_assoc + /-- #### Exercise 2.1 Assume that `A` is the set of integers divisible by `4`. Similarly assume that