diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index de1ed96..84052fc 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -421,6 +421,17 @@ \lean{Init/Prelude} {Mul.mul} +\section{\defined{Natural Map}}% +\hyperlabel{ref:natural-map} + + Let $R$ be an \nameref{ref:equivalence-relation} on $A$. + Then the \textbf{natural map} (or \textbf{canonical map}) + $\phi \colon A \rightarrow A / R$ is defined as $$\phi(x) = [x]_R$$ for + $x \in A$. + + \lean*{Init/Core} + {Quotient.lift} + \section{\defined{Natural Number}}% \hyperlabel{ref:natural-number} @@ -3072,6 +3083,9 @@ \code{Bookshelf/Enderton/Set/Relation} {Set.Relation.one\_to\_one\_comp\_is\_one\_to\_one} + \lean{Mathlib/Data/Set/Function} + {Set.InjOn.comp} + \begin{proof} Let $F \colon B \rightarrow C$ and $G \colon A \rightarrow B$ be one-to-one \nameref{ref:function}s from sets $A$, $B$, and $C$. @@ -3116,91 +3130,93 @@ \end{align*} \end{proof} -\subsection{\verified{Theorem 3J}}% -\hyperlabel{sub:theorem-3j} +\subsection{\verified{Theorem 3J (a)}}% +\hyperlabel{sub:theorem-3j-a} - \begin{theorem}[3J] + \begin{theorem}[3J(a)] Assume that $F \colon A \rightarrow B$, and that $A$ is nonempty. - \begin{enumerate}[(a)] - \item There exists a function $G \colon B \rightarrow A$ - (a "left inverse") such that $G \circ F$ is the identity function $I_A$ - on $A$ iff $F$ is one-to-one. - \item There exists a function $H \colon B \rightarrow A$ - (a "right inverse") such that $F \circ H$ is the identity function $I_B$ - on $B$ iff $F$ maps $A$ \textit{onto} $B$. - \end{enumerate} + There exists a function $G \colon B \rightarrow A$ (a "left inverse") such + that $G \circ F$ is the identity function $I_A$ on $A$ iff $F$ is + one-to-one. \end{theorem} \code{Bookshelf/Enderton/Set/Chapter\_3} {Enderton.Set.Chapter\_3.theorem\_3j\_a} + \begin{proof} + + Let $F$ be a \nameref{ref:function} from nonempty set $A$ to set $B$. + + \subparagraph{($\Rightarrow$)}% + + Let $G \colon B \rightarrow A$ such that $G \circ F = I_A$. + All that remains is to prove $F$ is single-rooted. + Let $y \in \ran{F}$. + By definition of the \nameref{ref:range} of a function, there exists + some $x_1$ such that $\tuple{x_1, y} \in F$. + Suppose there exists a set $x_2$ such that $\tuple{x_2, y} \in F$. + By hypothesis, $G(F(x_1)) = G(F(x_2))$ implies $I_A(x_1) = I_A(x_2)$. + Thus $x_1 = x_2$. + Therefore $F$ must be single-rooted. + + \subparagraph{($\Leftarrow$)}% + + Let $F$ be one-to-one. + Since $A$ is nonempty, there exists some $a \in A$. + Let $G \colon B \rightarrow A$ be given by + $$G(y) = \begin{cases} + F^{-1}(y) & \text{if } y \in \ran{F} \\ + a & \text{otherwise}. + \end{cases}$$ + $G$ is a function by virtue of \nameref{sub:one-to-one-inverse} and + choice of mapping for all values $y \not\in \ran{F}$. + Furthermore, for all $x \in A$, $F(x) \in \ran{F}$. + Thus $(G \circ F)(x) = G(F(x)) = F^{-1}(F(x)) = x$ by + \nameref{sub:theorem-3g}. + + \end{proof} + +\subsection{\unverified{Theorem 3J (b)}}% +\hyperlabel{sub:theorem-3j-b} + + \begin{theorem}[3J(b)] + Assume that $F \colon A \rightarrow B$, and that $A$ is nonempty. + There exists a function $H \colon B \rightarrow A$ (a "right inverse") such + that $F \circ H$ is the identity function $I_B$ on $B$ iff $F$ maps $A$ + \textit{onto} $B$. + \end{theorem} + \code{Bookshelf/Enderton/Set/Chapter\_3} {Enderton.Set.Chapter\_3.theorem\_3j\_b} \begin{proof} + Let $F$ be a \nameref{ref:function} from nonempty set $A$ to set $B$. - \paragraph{(a)}% + \subparagraph{($\Rightarrow$)}% - We prove there exists a function $G \colon B \rightarrow A$ such that - $G \circ F = I_A$ if and only if $F$ is one-to-one. + Suppose $H \colon B \rightarrow A$ such that $F \circ H = I_A$. + All that remains is to prove $\ran{F} = B$. + Note that $\ran{F} \subseteq B$ by hypothesis. + Let $y \in B$. + But $F(H(y)) = y$ meaning $y \in \ran{F}$. + Thus $B \subseteq \ran{F}$. + Since $\ran{F} \subseteq B$ and $B \subseteq \ran{F}$, $\ran{F} = B$. - \subparagraph{($\Rightarrow$)}% + \subparagraph{($\Leftarrow$)}% - Let $G \colon B \rightarrow A$ such that $G \circ F = I_A$. - All that remains is to prove $F$ is single-rooted. - Let $y \in \ran{F}$. - By definition of the \nameref{ref:range} of a function, there exists - some $x_1$ such that $\tuple{x_1, y} \in F$. - Suppose there exists a set $x_2$ such that $\tuple{x_2, y} \in F$. - By hypothesis, $G(F(x_1)) = G(F(x_2))$ implies $I_A(x_1) = I_A(x_2)$. - Thus $x_1 = x_2$. - Therefore $F$ must be single-rooted. - - \subparagraph{($\Leftarrow$)}% - - Let $F$ be one-to-one. - Since $A$ is nonempty, there exists some $a \in A$. - Let $G \colon B \rightarrow A$ be given by - $$G(y) = \begin{cases} - F^{-1}(y) & \text{if } y \in \ran{F} \\ - a & \text{otherwise}. - \end{cases}$$ - $G$ is a function by virtue of \nameref{sub:one-to-one-inverse} and - choice of mapping for all values $y \not\in \ran{F}$. - Furthermore, for all $x \in A$, $F(x) \in \ran{F}$. - Thus $(G \circ F)(x) = G(F(x)) = F^{-1}(F(x)) = x$ by - \nameref{sub:theorem-3g}. - - \paragraph{(b)}% - - We prove there exists a function $H \colon B \rightarrow A$ such that - $F \circ H = I_A$ if and only if $F$ maps $A$ onto $B$. - - \subparagraph{($\Rightarrow$)}% - - Suppose $H \colon B \rightarrow A$ such that $F \circ H = I_A$. - All that remains is to prove $\ran{F} = B$. - Note that $\ran{F} \subseteq B$ by hypothesis. - Let $y \in B$. - But $F(H(y)) = y$ meaning $y \in \ran{F}$. - Thus $B \subseteq \ran{F}$. - Since $\ran{F} \subseteq B$ and $B \subseteq \ran{F}$, $\ran{F} = B$. - - \subparagraph{($\Leftarrow$)}% - - Suppose $F$ maps $A$ \textit{onto} $B$. - By definition of maps onto, $\ran{F} = B$. - Then for all $y \in B$, there exists some $x \in A$ such that - $\tuple{x, y} \in F$. - Notice though that $F^{-1}[\{y\}]$ may not be a singleton set. - Then there is no obvious way to \textit{choose} an element from each - preimage to form a function. - By the \nameref{ref:axiom-of-choice-1}, there exists a function - $H \subseteq F^{-1}$ such that $\dom{H} = \dom{F^{-1}} = B$. - For all $y \in B$, $\tuple{y, H(y)} \in H \subseteq F^{-1}$ - meaning $\tuple{H(y), y} \in F$. - Thus $F(H(y)) = y$ as expected. + Suppose $F$ maps $A$ \textit{onto} $B$. + By definition of maps onto, $\ran{F} = B$. + Then for all $y \in B$, there exists some $x \in A$ such that + $\tuple{x, y} \in F$. + Notice though that $F^{-1}[\{y\}]$ may not be a singleton set. + Then there is no obvious way to \textit{choose} an element from each + preimage to form a function. + By the \nameref{ref:axiom-of-choice-1}, there exists a function + $H \subseteq F^{-1}$ such that $\dom{H} = \dom{F^{-1}} = B$. + For all $y \in B$, $\tuple{y, H(y)} \in H \subseteq F^{-1}$ + meaning $\tuple{H(y), y} \in F$. + Thus $F(H(y)) = y$ as expected. \end{proof} @@ -3215,9 +3231,9 @@ \begin{proof} By definition, a one-to-one correspondence $f$ between sets $A$ and $B$ must be both one-to-one and onto. - By \nameref{sub:theorem-3j}, $f$ is one-to-one if and only if it has a left - inverse. - The same theorem states that $f$ is onto $B$ if and only if it has a right + By \nameref{sub:theorem-3j-a}, $f$ is one-to-one if and only if it has a + left inverse. + By \nameref{sub:theorem-3j-b}, $f$ is onto $B$ if and only if it has a right inverse. \end{proof} @@ -9099,7 +9115,7 @@ \hyperlabel{sub:lemma-6f} \begin{lemma}[6F] - If $C$ is a proper subset of a natural number $n$, then $C \approx m$ for + If $C$ is a proper subset of a natural number $n$, then $C \equin m$ for some $m$ less than $n$. \end{lemma} @@ -9199,6 +9215,214 @@ Hence $S'$ is a finite set. \end{proof} +\subsection{\verified{Subset Size}}% +\hyperlabel{sub:subset-size} + + \begin{lemma} + Let $A$ be a finite set and $B \subseteq A$. + Then there exist natural numbers $m, n \in \omega$ such that + $B \equin m$, $A \equin n$, and $m \leq n$. + \end{lemma} + + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.subset\_size} + + \begin{proof} + + Let $A$ be a \nameref{ref:finite-set} and $B$ be a subset of $A$. + By \nameref{sub:corollary-6g}, $B$ must be finite. + By definition of a finite set, there exists natural numbers + $m, n \in \omega$ such that $B \equin m$ and $A \equin n$. + By \nameref{sub:trichotomy-law-natural-numbers}, it suffices to prove that + $m > n$ is not possible for then either $m < n$ or $m = n$. + + For the sake of contradiction, assume $m > n$. + By definition of \nameref{ref:equinumerous}, there exists a one-to-one + correspondence between $B$ and $m$. + \nameref{sub:theorem-6a} indicates there then exists a one-to-one + correspondence $f$ between $m$ and $B$. + Likewise, there exists a one-to-one correspondence $g$ between $A$ and + $n$. + + Define $h \colon A \rightarrow B$ as $h(x) = f(g(x))$ for all $x \in A$. + Since $n \subset m$ by \nameref{sub:corollary-4m}, $h$ is well-defined. + By \nameref{sub:one-to-one-composition}, $h$ must be one-to-one. + Thus $h$ is a one-to-one correspondence between $A$ and $\ran{h}$, i.e. + $A \equin \ran{h}$. + But $n < m$ meaning $\ran{h} \subset B$ which in turn is a proper subset + of $A$ by hypothesis. + \nameref{sub:corollary-6c} states no finite set is equinumerous to a + proper subset of itself, a contradiction. + + \end{proof} + +\subsection{\pending{Finite Domain and Range Size}}% +\hyperlabel{sub:finite-domain-range-size} + + \begin{lemma} + Let $A$ and $B$ be finite sets and $f \colon A \rightarrow B$ be a function. + Then there exist natural numbers $m, n \in \omega$ such that + $\dom{f} \equin m$, $\ran{f} \equin n$, and $m \geq n$. + \end{lemma} + + \begin{note} + This proof avoids the \nameref{ref:axiom-of-choice-1} because $A$ and $B$ + are finite. + In particular, we are able to choose a "smallest" element of each preimage + set. + Contrast this to \nameref{sub:theorem-3j-b}. + \end{note} + + \begin{proof} + Let $A$ and $B$ be \nameref{ref:finite-set}s and $f \colon A \rightarrow B$ + be a function. + By definition of finite sets, there exists \nameref{ref:natural-number}s + $m, p \in \omega$ such that $A \equin m$ and $B \equin p$. + By definition of the \nameref{ref:domain} of a function, $\dom{f} = A$. + Thus $\dom{f} \equin m$. + + By \nameref{sub:theorem-6a}, there exists a one-to-one correspondence $g$ + between $m$ and $\dom{f} = A$. + For all $y \in \ran{f}$, consider $\img{f^{-1}}{\{y\}}$. + Let $$A_y = \{ x \in m \mid f(g(x)) = y \}.$$ + Since $g$ is a one-to-one correspondence, it follows that + $A_y \equin \img{f^{-1}}{\{y\}}$. + Since $A_y$ is a nonempty subset of natural numbers, the + \nameref{sub:well-ordering-natural-numbers} implies there exists a least + element, say $q_y$. + Define $C = \{q_y \mid y \in \ran{f}\}$. + Thus $h \colon C \rightarrow \ran{f}$ given by $h(x) = f(g(x))$ is a + one-to-one correspondence between $C$ and $\ran{f}$ by construction. + That is, $C \equin \ran{f}$. + By \nameref{sub:lemma-6f}, there exists some $n \leq m$ such that + $C \equin n$. + By \nameref{sub:theorem-6a}, $n \equin \ran{f}$. + \end{proof} + +\subsection{\pending{Set Difference Size}}% +\hyperlabel{sub:set-difference-size} + + \begin{lemma} + Let $A \equin m$ for some natural number $m$ and $B \subseteq A$. + Then there exists some $n \in \omega$ such that $B \equin n$ and + $A - B \equin m - n$. + \end{lemma} + + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.sdiff\_size} + + TODO: Update IH and add additional lemmas to fully prove this out. + + \begin{proof} + + Let + \begin{equation} + \hyperlabel{sub:set-difference-size-ih} + S = \{m \in \omega \mid + \forall A \equin m, \forall B \subseteq A, \exists n + \in \omega (B \equin n \land A - B \equin m - n)\}. + \end{equation} + We prove that (i) $0 \in S$ and (ii) if $n \in S$ then $n^+ \in S$. + Afterward we prove (iii) the lemma statement. + + \paragraph{(i)}% + \hyperlabel{par:set-difference-size-i} + + Let $A \equin 0$ and $B \subseteq A$. + Then it follows $A = B = \emptyset$. + Therefore $B \equin 0$ and $$A - B = \emptyset \equin 0 = 0 - 0$$ as + expected. + + \paragraph{(ii)}% + \hyperlabel{par:set-difference-size-ii} + + Suppose $m \in S$ and consider $m^+$. + Let $A \equin m^+$ and let $B \subseteq A$. + By definition of \nameref{ref:equinumerous}, there exists a one-to-one + correspondence $f$ between $A$ and $m^+$. + Since $f$ is one-to-one and onto, there exists a unique value $a \in A$ + such that $f(a) = m$. + Then $B - \{a\} \subseteq A - \{a\}$ and $f$ is a one-to-one + correspondence between $A - \{a\}$ and $m$. + By \ihref{sub:set-difference-size-ih}, there exists some $n \in \omega$ + such that $B - \{a\} \equin n$ and + \begin{equation} + \hyperlabel{par:set-difference-size-ii-eq1} + (A - \{a\}) - (B - \{a\}) \equin m - n. + \end{equation} + There are two cases to consider: + + \subparagraph{Case 1}% + + Assume $a \in B$. + Then $B \equin n^+$. + Furthermore, by definition of the set difference, + \begin{align} + (A - \{a\}) & - (B - \{a\}) \nonumber \\ + & = \{x \mid + x \in A - \{a\} \land x \not\in B - \{a\}\} \nonumber \\ + & = \{x \mid + (x \in A \land x \neq a) \land + \neg(x \in B \land x \neq a)\} \nonumber \\ + & = \{x \mid + (x \in A \land x \neq a) \land + (x \not\in B \lor x = a)\} \nonumber \\ + & = \{x \mid + (x \in A \land x \neq a \land x \not\in B) \lor + (x \in A \land x \neq a \land x = a)\} \nonumber \\ + & = \{x \mid + (x \in A \land x \neq a \land x \not\in B) \lor F\} \nonumber \\ + & = \{x \mid + (x \in A \land x \neq a \land x \not\in B)\} \nonumber \\ + & = \{x \mid x \in A - B \land x \neq a\} \nonumber \\ + & = \{x \mid x \in A - B \land x \not\in \{a\}\} \nonumber \\ + & = (A - B) - \{a\}. + \label{par:set-difference-size-ii-eq2} + \end{align} + Since $a \in A$ and $a \in B$, $(A - B) - \{a\} = A - B$. + Thus + \begin{align*} + (A - \{a\} - (B - \{a\}) + & = (A - B) - \{a\} & \eqref{par:set-difference-size-ii-eq2} \\ + & = A - B \\ + & \equin m - n & \eqref{par:set-difference-size-ii-eq1} \\ + & \equin m^+ - n^+ & \textref{sub:theorem-6a}. + \end{align*} + + \subparagraph{Case 2}% + + Assume $a \not\in B$. + Then $B - \{a\} = B$ (i.e. $B \approx n$) and + \begin{align*} + (A - \{a\}) - (B - \{a\}) + & = (A - \{a\}) - B \\ + & \equin m - n & \eqref{par:set-difference-size-ii-eq1}. + \end{align*} + The above implies that there exists a one-to-one correspondence $g$ + between $(A - \{a\}) - B$ and $m - n$. + Therefore $g \cup \{\tuple{a, m}\}$ is a one-to-one correspondence + between $A - B$ and $(m - n) \cup \{m\}$. + By \nameref{sub:theorem-6a}, + $$A - B \equin (m - n) \cup \{m\} \equin m^+ - n.$$ + + \subparagraph{Subconclusion}% + + The above two cases are exhaustive and both conclude the existence of + some $n \in \omega$ such that $B \equin n$ and $A - B \equin m^+ - n$. + Hence $m^+ \in S$. + + \paragraph{(iii)}% + + By \nameref{par:set-difference-size-i} and + \nameref{par:set-difference-size-ii}, $S \subseteq \omega$ is an + \nameref{ref:inductive-set}. + Thus \nameref{sub:theorem-4b} implies $S = \omega$. + Hence, for all $A \equin m$ for some $m \in \omega$, if $B \subseteq A$, + then there exists some $n \in \omega$ such that $B \equin n$ and + $A - B \equin m - n$. + + \end{proof} + \subsection{\sorry{Theorem 6H}}% \hyperlabel{sub:theorem-6h} @@ -9601,8 +9825,33 @@ \paragraph{($\Leftarrow$)}% - Suppose $\ran{f} = A$. - TODO: by induction? + If $A = \emptyset$, then $f$ is trivially one-to-one. + Assume now $A \neq \emptyset$ and $\ran{f} = A$. + Let $x_1, x_2 \in A$ such that $f(x_1) = f(x_2) = y$ for some $y \in A$. + We must prove that $x_1 = x_2$. + + Let $B = \img{f^{-1}}{\{y\}}$. + Then $x_1, x_2 \in B$. + Since $B \subseteq A$, \nameref{sub:subset-size} indicates that there + exist natural numbers $m_1, n_1 \in \omega$ such that $B \equin m_1$, + $A \equin n_1$, and $m_1 \leq n_1$. + Define $f' \colon (A - B) \rightarrow (A - \{y\})$ as the + \nameref{ref:restriction} of $f$ to $A - B$. + Since $\ran{f} = A$, it follows $\ran{f'} = A - \{y\}$. + Since \nameref{sub:corollary-6g} implies $A - B$ and $A - \{y\}$ are + finite sets, \nameref{sub:finite-domain-range-size} implies the + existence of natural numbers $m_2, n_2 \in \omega$ such that + $\dom{f'} \equin m_2$, $\ran{f'} \equin n_2$, and $m_2 \geq n_2$. + Thus, by \nameref{sub:set-difference-size}, + \begin{align*} + m_2 & \equin \dom{f'} \equin A - B \equin n_1 - m_1 \\ + n_2 & \equin \ran{f'} \equin A - \{y\} \equin n_1 - 1. + \end{align*} + By \nameref{sub:corollary-6e}, $m_2 = n_1 - m_1$ and $n_2 = n_1 - 1$. + Since $m_2 \geq n_2$, $n_1 - m_1 \geq n_1 - 1$. + But $1 \leq m_1 \leq n_1$ meaning $m_1 = 1$. + Hence $B$ is a singleton. + Therefore $x_1 = x_2$, i.e. $f$ is one-to-one. \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index d86e218..c6938e6 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -264,7 +264,7 @@ theorem theorem_3j_a {F : Set.HRelation α β} Assume that `F : A → B`, and that `A` is nonempty. There exists a function `H : B → A` (a "right inverse") such that `F ∘ H` is the identity function on -`B` **iff** `F` maps `A` onto `B`. +`B` only if `F` maps `A` onto `B`. -/ theorem theorem_3j_b {F : Set.HRelation α β} (hF : mapsInto F A B) : (∃ H, mapsInto H B A ∧ comp F H = { p | p.1 ∈ B ∧ p.1 = p.2 }) → diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean index 685cfb2..df7dd56 100644 --- a/Bookshelf/Enderton/Set/Chapter_6.lean +++ b/Bookshelf/Enderton/Set/Chapter_6.lean @@ -3,10 +3,10 @@ import Common.Logic.Basic import Common.Nat.Basic import Common.Set.Basic import Common.Set.Equinumerous +import Common.Set.Function import Common.Set.Intervals import Mathlib.Data.Finset.Card import Mathlib.Data.Set.Finite -import Mathlib.Tactic.LibrarySearch /-! # Enderton.Set.Chapter_6 @@ -83,11 +83,8 @@ lemma pigeonhole_principle_aux (n : ℕ) 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) + · rw [hM', Set.SurjOn_emptyset_Iio_iff_eq_zero] at hf_surj + simp at hf_surj by_cases h : ¬ ∃ t, t ∈ M ∧ f t = n -- Trivial case. `f` must not be onto if this is the case. @@ -95,17 +92,18 @@ lemma pigeonhole_principle_aux (n : ℕ) exact absurd ⟨t, ht⟩ h -- Continue under the assumption `n ∈ ran f`. - simp only [not_not] at h - have ⟨t, ht₁, ht₂⟩ := h + have ⟨t, ht₁, ht₂⟩ := not_not.mp h - -- `M ≠ ∅` so `∃ p, ∀ x ∈ M, p ≥ x`. + -- `M ≠ ∅` so `∃ p, ∀ x ∈ M, p ≥ x`, i.e. a maximum member. 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) + · show Set.Finite M + 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] + · show Set.Nonempty M + exact Set.nmem_singleton_empty.mp hM' + · show M ⊆ M + exact Eq.subset rfl -- `g` is a variant of `f` in which the largest element of its domain -- (i.e. `p`) corresponds to value `n`. @@ -675,6 +673,349 @@ theorem corollary_6g {S S' : Set α} (hS : Set.Finite S) (hS' : S' ⊆ S) · intro h rwa [h] +/-- #### Subset Size + +Let `A` be a finite set and `B ⊂ A`. Then there exist natural numbers `m, n ∈ ω` +such that `B ≈ m`, `A ≈ n`, and `m ≤ n`. +-/ +lemma subset_size [DecidableEq α] [Nonempty α] {A B : Set α} + (hBA : B ⊆ A) (hA : Set.Finite A) + : ∃ m n : ℕ, B ≈ Set.Iio m ∧ A ≈ Set.Iio n ∧ m ≤ n := by + have ⟨n, hn⟩ := Set.finite_iff_equinumerous_nat.mp hA + have ⟨m, hm⟩ := Set.finite_iff_equinumerous_nat.mp (corollary_6g hA hBA) + refine ⟨m, n, hm, hn, ?_⟩ + + suffices ¬ m > n by + match @trichotomous ℕ LT.lt _ m n with + | Or.inr (Or.inl hr) => -- m = n + rw [hr] + | Or.inr (Or.inr hr) => -- m > n + exact absurd hr this + | Or.inl hr => -- m < n + exact Nat.le_of_lt hr + + by_contra nr + have ⟨f, hf⟩ := Set.equinumerous_symm hm + have ⟨g, hg⟩ := hn + + let h x := f (g x) + have hh : Set.BijOn h A (h '' A) := by + refine ⟨?_, ?_, Eq.subset rfl⟩ + · -- `Set.MapsTo h A (ran h)` + intro x hx + simp only [Set.mem_image] + exact ⟨x, hx, rfl⟩ + · -- `Set.InjOn h A` + refine Set.InjOn.comp hf.right.left hg.right.left ?_ + intro x hx + exact Nat.lt_trans (hg.left hx) nr + + have : h '' A ⊂ A := by + rw [Set.ssubset_def] + apply And.intro + · show ∀ x, x ∈ h '' A → x ∈ A + intro x hx + have ⟨y, hy₁, hy₂⟩ := hx + have h₁ : g y ∈ Set.Iio n := hg.left hy₁ + have h₂ : f (g y) ∈ B := hf.left (Nat.lt_trans h₁ nr) + have h₃ : x ∈ B := by rwa [← hy₂] + exact hBA h₃ + · rw [Set.subset_def] + simp only [Set.mem_image, not_forall, not_exists, not_and, exists_prop] + refine ⟨f n, hBA (hf.left nr), ?_⟩ + intro x hx + by_contra nh + have h₁ : g x < n := hg.left hx + have h₂ : g x ∈ Set.Iio m := Nat.lt_trans h₁ nr + rw [hf.right.left h₂ nr nh] at h₁ + simp at h₁ + exact absurd ⟨h, hh⟩ (corollary_6c hA this) + +/-- #### Finite Domain and Range Size + +Let `A` and `B` be finite sets and `f : A → B` be a function. Then there exist +natural numbers `m, n ∈ ω` such that `dom f ≈ m`, `ran f ≈ n`, and `m ≥ n`. +-/ +theorem finite_dom_ran_size [Nonempty α] {A B : Set α} + (hA : Set.Finite A) (hB : Set.Finite B) (hf : Set.MapsTo f A B) + : ∃ m n : ℕ, A ≈ Set.Iio m ∧ f '' A ≈ Set.Iio n ∧ m ≥ n := by + have ⟨m, hm⟩ := Set.finite_iff_equinumerous_nat.mp hA + have ⟨p, hp⟩ := Set.finite_iff_equinumerous_nat.mp hB + have ⟨g, hg⟩ := Set.equinumerous_symm hm + + let A_y y := { x ∈ Set.Iio m | f (g x) = y } + have hA₁ : ∀ y ∈ B, A_y y ≈ f ⁻¹' {y} := by + sorry + have hA₂ : ∀ y ∈ B, Set.Nonempty (A_y y) := by + sorry + have hA₃ : ∀ y ∈ B, ∃ q : ℕ, ∀ p ∈ A_y y, q ≤ p := by + sorry + + let C := { q | ∃ y ∈ B, ∀ p ∈ A_y y, q ≤ p } + let h x := f (g x) + have hh : C ≈ f '' A := by + sorry + + sorry + +/-- #### Set Difference Size + +Let `A ≈ m` for some natural number `m` and `B ⊆ A`. Then there exists some +`n ∈ ω` such that `B ≈ n` and `A - B ≈ m - n`. +-/ +lemma sdiff_size_aux [DecidableEq α] [Nonempty α] + : ∀ A : Set α, A ≈ Set.Iio m → + ∀ B, B ⊆ A → + ∃ n : ℕ, n ≤ m ∧ B ≈ Set.Iio n ∧ A \ B ≈ (Set.Iio m) \ (Set.Iio n) := by + induction m with + | zero => + intro A hA B hB + refine ⟨0, ?_⟩ + simp only [ + Nat.zero_eq, + sdiff_self, + Set.bot_eq_empty, + Set.equinumerous_zero_iff_emptyset + ] at hA ⊢ + have hB' : B = ∅ := Set.subset_eq_empty hB hA + have : A \ B = ∅ := by + rw [hB'] + simp only [Set.diff_empty] + exact hA + rw [this] + refine ⟨trivial, hB', Set.equinumerous_emptyset_emptyset⟩ + + | succ m ih => + intro A ⟨f, hf⟩ B hB + + -- Since `f` is one-to-one and onto, there exists a unique value `a ∈ A` + -- such that `f(a) = m`. + have hfa := hf.right.right + unfold Set.SurjOn at hfa + have ⟨a, ha₁, ha₂⟩ := (Set.subset_def ▸ hfa) m (by simp) + + -- `f` is a one-to-one correspondence between `A - {a}` and `m`. + have hBA : B \ {a} ⊆ A \ {a} := Set.diff_subset_diff_left hB + have hfBA : Set.BijOn f (A \ {a}) (Set.Iio m) := by + refine ⟨?_, ?_, ?_⟩ + · intro x hx + have := hf.left hx.left + simp only [Set.mem_Iio, gt_iff_lt] at this ⊢ + apply Or.elim (Nat.lt_or_eq_of_lt this) + · simp + · intro h + rw [← ha₂] at h + exact absurd (hf.right.left hx.left ha₁ h) hx.right + · intro x₁ hx₁ x₂ hx₂ h + exact hf.right.left hx₁.left hx₂.left h + · have := hf.right.right + unfold Set.SurjOn Set.image at this ⊢ + rw [Set.subset_def] at this ⊢ + simp only [ + Set.mem_Iio, + Set.mem_diff, + Set.mem_singleton_iff, + Set.mem_setOf_eq + ] at this ⊢ + intro x hx + have ⟨b, hb⟩ := this x (Nat.lt.step hx) + refine ⟨b, ⟨hb.left, ?_⟩, hb.right⟩ + by_contra nb + rw [← nb, hb.right] at ha₂ + exact absurd ha₂ (Nat.ne_of_lt hx) + + -- `(A - {a}) - (B - {a}) ≈ m - n` + have ⟨n, hn₁, hn₂, hn₃⟩ := ih (A \ {a}) ⟨f, hfBA⟩ (B \ {a}) hBA + by_cases hc : a ∈ B + + · refine ⟨n.succ, ?_, ?_, ?_⟩ + · exact Nat.succ_le_succ hn₁ + · -- `B ≈ Set.Iio n.succ` + have ⟨g, hg⟩ := hn₂ + let g' x := if x = a then n else g x + refine ⟨g', ⟨?_, ?_, ?_⟩⟩ + · -- `Set.MapsTo g' B (Set.Iio n.succ)` + intro x hx + dsimp only + by_cases hx' : x = a + · rw [if_pos hx'] + simp + · rw [if_neg hx'] + calc g x + _ < n := hg.left ⟨hx, hx'⟩ + _ < n + 1 := by simp + · -- `Set.InjOn g' B` + intro x₁ hx₁ x₂ hx₂ h + dsimp only at h + by_cases hc₁ : x₁ = a <;> by_cases hc₂ : x₂ = a + · rw [hc₁, hc₂] + · rw [if_pos hc₁, if_neg hc₂] at h + exact absurd h.symm (Nat.ne_of_lt $ hg.left ⟨hx₂, hc₂⟩) + · rw [if_neg hc₁, if_pos hc₂] at h + exact absurd h (Nat.ne_of_lt $ hg.left ⟨hx₁, hc₁⟩) + · rw [if_neg hc₁, if_neg hc₂] at h + exact hg.right.left ⟨hx₁, hc₁⟩ ⟨hx₂, hc₂⟩ h + · -- `Set.SurjOn g' B (Set.Iio n.succ)` + have := hg.right.right + unfold Set.SurjOn Set.image at this ⊢ + rw [Set.subset_def] at this ⊢ + simp only [Set.mem_Iio, Set.mem_setOf_eq] at this ⊢ + intro x hx + by_cases hc₁ : x = n + · refine ⟨a, hc, ?_⟩ + simp only [ite_true] + exact hc₁.symm + · apply Or.elim (Nat.lt_or_eq_of_lt hx) + · intro hx₁ + have ⟨b, ⟨hb₁, hb₂⟩, hb₃⟩ := this x hx₁ + refine ⟨b, hb₁, ?_⟩ + simp only [Set.mem_singleton_iff] at hb₂ + rwa [if_neg hb₂] + · intro hx₁ + exact absurd hx₁ hc₁ + · have hA₁ : (A \ {a}) \ (B \ {a}) = (A \ B) \ {a} := + Set.diff_mem_diff_mem_eq_diff_diff_mem + have hA₂ : (A \ B) \ {a} = A \ B := by + refine Set.not_mem_diff_eq_self ?_ + by_contra na + exact absurd hc na.right + rw [hA₁, hA₂] at hn₃ + suffices (Set.Iio m) \ (Set.Iio n) ≈ (Set.Iio m.succ) \ (Set.Iio n.succ) + from Set.equinumerous_trans hn₃ this + -- `m - n ≈ m⁺ - n⁺` + refine ⟨fun x => x + 1, ?_, ?_, ?_⟩ + · intro x ⟨hx₁, hx₂⟩ + simp at hx₁ hx₂ ⊢ + exact ⟨Nat.le_add_of_sub_le hx₂, Nat.add_lt_of_lt_sub hx₁⟩ + · intro _ _ _ _ h + simp only [add_left_inj] at h + exact h + · unfold Set.SurjOn Set.image + rw [Set.subset_def] + intro x ⟨hx₁, hx₂⟩ + simp only [ + Set.Iio_diff_Iio, + gt_iff_lt, + not_lt, + ge_iff_le, + Set.mem_setOf_eq, + Set.mem_Iio + ] at hx₁ hx₂ ⊢ + have ⟨p, hp⟩ : ∃ p : ℕ, x = p.succ := by + refine Nat.exists_eq_succ_of_ne_zero ?_ + have := calc 0 + _ < n.succ := by simp + _ ≤ x := hx₂ + exact Nat.pos_iff_ne_zero.mp this + refine ⟨p, ⟨?_, ?_⟩, hp.symm⟩ + · rw [hp] at hx₂ + exact Nat.lt_succ.mp hx₂ + · rw [hp] at hx₁ + exact Nat.succ_lt_succ_iff.mp hx₁ + + · have hB : B \ {a} = B := Set.not_mem_diff_eq_self hc + refine ⟨n, ?_, ?_, ?_⟩ + · calc n + _ ≤ m := hn₁ + _ ≤ m + 1 := by simp + · rwa [← hB] + · rw [hB] at hn₃ + have ⟨g, hg⟩ := hn₃ + have hAB : A \ B ≈ (Set.Iio m) \ (Set.Iio n) ∪ {m} := by + refine ⟨fun x => if x = a then m else g x, ?_, ?_, ?_⟩ + · intro x hx + dsimp only + by_cases hc₁ : x = a + · rw [if_pos hc₁] + simp + · rw [if_neg hc₁] + have := hg.left ⟨⟨hx.left, hc₁⟩, hx.right⟩ + simp only [ + Set.Iio_diff_Iio, + gt_iff_lt, + not_lt, + ge_iff_le, + Set.union_singleton, + Set.mem_Ico, + lt_self_iff_false, + and_false, + Set.mem_insert_iff + ] at this ⊢ + right + exact this + · intro x₁ hx₁ x₂ hx₂ h + dsimp only at h + by_cases hc₁ : x₁ = a <;> by_cases hc₂ : x₂ = a + · rw [hc₁, hc₂] + · rw [if_pos hc₁, if_neg hc₂] at h + have := hg.left ⟨⟨hx₂.left, hc₂⟩, hx₂.right⟩ + simp at this + exact absurd h.symm (Nat.ne_of_lt this.right) + · rw [if_neg hc₁, if_pos hc₂] at h + have := hg.left ⟨⟨hx₁.left, hc₁⟩, hx₁.right⟩ + simp at this + exact absurd h (Nat.ne_of_lt this.right) + · rw [if_neg hc₁, if_neg hc₂] at h + exact hg.right.left ⟨⟨hx₁.left, hc₁⟩, hx₁.right⟩ ⟨⟨hx₂.left, hc₂⟩, hx₂.right⟩ h + · have := hg.right.right + unfold Set.SurjOn Set.image at this ⊢ + rw [Set.subset_def] at this ⊢ + simp at this ⊢ + refine ⟨⟨a, ⟨ha₁, hc⟩, ?_⟩, ?_⟩ + · intro ha + simp at ha + · intro x hx₁ hx₂ + have ⟨y, hy₁, hy₂⟩ := this x hx₁ hx₂ + refine ⟨y, ?_, ?_⟩ + · exact ⟨hy₁.left.left, hy₁.right⟩ + · rwa [if_neg hy₁.left.right] + + suffices (Set.Iio m) \ (Set.Iio n) ∪ {m} ≈ (Set.Iio m.succ) \ (Set.Iio n) + from Set.equinumerous_trans hAB this + + refine ⟨fun x => x, ?_, ?_, ?_⟩ + · intro x hx + simp at hx ⊢ + apply Or.elim hx + · intro hx₁ + rw [hx₁] + exact ⟨hn₁, by simp⟩ + · intro ⟨hx₁, hx₂⟩ + exact ⟨hx₁, calc x + _ < m := hx₂ + _ < m + 1 := by simp⟩ + · intro _ _ _ _ h + exact h + · unfold Set.SurjOn Set.image + rw [Set.subset_def] + simp only [ + Set.Iio_diff_Iio, + gt_iff_lt, + not_lt, + ge_iff_le, + Set.mem_Ico, + Set.union_singleton, + lt_self_iff_false, + and_false, + Set.mem_insert_iff, + exists_eq_right, + Set.mem_setOf_eq, + and_imp + ] + intro x hn hm + apply Or.elim (Nat.lt_or_eq_of_lt hm) + · intro hx + right + exact ⟨hn, hx⟩ + · intro hx + left + exact hx + +lemma sdiff_size [DecidableEq α] [Nonempty α] {A B : Set α} + (hB : B ⊆ A) (hA : A ≈ Set.Iio m) + : ∃ n : ℕ, n ≤ m ∧ B ≈ Set.Iio n ∧ A \ B ≈ (Set.Iio m) \ (Set.Iio n) := + sdiff_size_aux A hA B hB + /-- #### Exercise 6.7 Assume that `A` is finite and `f : A → A`. Show that `f` is one-to-one **iff** @@ -702,7 +1043,27 @@ theorem exercise_6_7 [DecidableEq α] [Nonempty α] {A : Set α} {f : α → α} rw [subset_iff_ssubset_or_eq] at hf₃ exact Or.elim hf₃ (fun h => absurd hf₂ (corollary_6c hA₁ h)) id · intro hf₁ - sorry + by_cases hA₃ : A = ∅ + · rw [hA₃] + simp + · intro x₁ hx₁ x₂ hx₂ hf₂ + let y := f x₁ + let B := f ⁻¹' {y} + have hB₁ : x₁ ∈ B := sorry + have hB₂ : x₂ ∈ B := sorry + have hB₃ : B ⊆ A := sorry + have ⟨m₁, n₁, hm₁, hn₁, hmn₁⟩ := subset_size hB₃ hA₁ + + have hf'₁ : Set.MapsTo f (A \ B) (A \ {y}) := sorry + have hf'₂ : f '' (A \ B) = A \ {y} := sorry + have hf'₃ : Set.Finite (A \ B) := sorry + have hf'₄ : Set.Finite (A \ {y}) := sorry + + have ⟨m₂, n₂, hm₂, hn₂, hmn₂⟩ := finite_dom_ran_size hf'₃ hf'₄ hf'₁ + + have h₁ : A \ B ≈ Set.Iio (n₁ - m₁) := sorry + have h₂ : A \ {y} ≈ Set.Iio (n₁ - 1) := sorry + sorry /-- #### Exercise 6.8 diff --git a/Common/Set.lean b/Common/Set.lean index ef5f266..4c3e6be 100644 --- a/Common/Set.lean +++ b/Common/Set.lean @@ -1,4 +1,5 @@ import Common.Set.Basic import Common.Set.Equinumerous +import Common.Set.Function 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 51d3d92..5dfc1be 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -193,6 +193,62 @@ theorem diff_ssubset_nonempty {A B : Set α} (h : A ⊂ B) · intro hx exact ⟨x, hx⟩ +/-- +If an element `x` is not a member of a set `A`, then `A - {x} = A`. +-/ +theorem not_mem_diff_eq_self {A : Set α} (h : a ∉ A) + : A \ {a} = A := by + ext x + apply Iff.intro + · exact And.left + · intro hx + refine ⟨hx, ?_⟩ + simp only [mem_singleton_iff] + by_contra nx + rw [nx] at hx + exact absurd hx h + +/-- +Given two sets `A` and `B`, `(A - {a}) - (B - {b}) = (A - B) - {a}`. +-/ +theorem diff_mem_diff_mem_eq_diff_diff_mem {A B : Set α} {a : α} + : (A \ {a}) \ (B \ {a}) = (A \ B) \ {a} := by + calc (A \ {a}) \ (B \ {a}) + _ = { x | x ∈ A \ {a} ∧ x ∉ B \ {a} } := rfl + _ = { x | x ∈ A \ {a} ∧ ¬(x ∈ B \ {a}) } := rfl + _ = { x | (x ∈ A ∧ x ≠ a) ∧ ¬(x ∈ B ∧ x ≠ a) } := rfl + _ = { x | (x ∈ A ∧ x ≠ a) ∧ (x ∉ B ∨ x = a) } := by + ext x + rw [mem_setOf_eq, not_and_de_morgan] + simp + _ = { x | (x ∈ A ∧ x ≠ a ∧ x ∉ B) ∨ (x ∈ A ∧ x ≠ a ∧ x = a) } := by + ext x + simp only [mem_setOf_eq] + rw [and_or_left, and_assoc, and_assoc] + _ = { x | x ∈ A ∧ x ≠ a ∧ x ∉ B } := by simp + _ = { x | x ∈ A ∧ x ∉ B ∧ x ≠ a } := by + ext x + simp only [ne_eq, sep_and, mem_inter_iff, mem_setOf_eq] + apply Iff.intro <;> + · intro ⟨⟨_, hx₂⟩, hx₃, hx₄⟩ + exact ⟨⟨hx₃, hx₄⟩, ⟨hx₃, hx₂⟩⟩ + _ = { x | x ∈ A ∧ x ∉ B ∧ x ∉ ({a} : Set α) } := rfl + _ = { x | x ∈ A \ B ∧ x ∉ ({a} : Set α) } := by + ext x + simp only [ + mem_singleton_iff, + sep_and, + mem_inter_iff, + mem_setOf_eq, + mem_diff, + and_congr_right_iff, + and_iff_right_iff_imp, + and_imp + ] + intro hx _ _ + exact hx + _ = (A \ B) \ {a} := rfl + /-- 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 index 6351a0f..a271fa6 100644 --- a/Common/Set/Equinumerous.lean +++ b/Common/Set/Equinumerous.lean @@ -8,6 +8,8 @@ Additional theorems around finite sets. namespace Set +/-! ### Definitions -/ + /-- 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`. @@ -19,6 +21,26 @@ infix:50 " ≈ " => Equinumerous theorem equinumerous_def (A : Set α) (B : Set β) : A ≈ B ↔ ∃ F, Set.BijOn F A B := Iff.rfl +/-- +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 + /-- For any set `A`, `A ≈ A`. -/ @@ -57,30 +79,53 @@ theorem eq_imp_equinumerous {A B : Set α} (h : A = B) conv at this => right; rw [h] exact this +/-! ### Finite Sets -/ + /-- 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 +/-! ### Emptyset -/ + /-- -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`. +Any set equinumerous to the emptyset is the emptyset. -/ -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 +theorem equinumerous_zero_iff_emptyset {S : Set α} + : S ≈ Set.Iio 0 ↔ S = ∅ := by apply Iff.intro + · intro ⟨f, hf⟩ + by_contra nh + rw [← Ne.def, ← Set.nonempty_iff_ne_empty] at nh + have ⟨x, hx⟩ := nh + have := hf.left hx + simp at this · 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 + rw [h] + refine ⟨fun _ => ⊥, ?_, ?_, ?_⟩ + · intro _ hx + simp at hx + · intro _ hx + simp at hx + · unfold SurjOn + simp only [bot_eq_zero', image_empty] + show ∀ x, x ∈ Set.Iio 0 → x ∈ ∅ + intro _ hx + simp at hx + +/-- +Empty sets are always equinumerous, regardless of their underlying type. +-/ +theorem equinumerous_emptyset_emptyset [Bot β] + : (∅ : Set α) ≈ (∅ : Set β) := by + refine ⟨fun _ => ⊥, ?_, ?_, ?_⟩ + · intro _ hx + simp at hx + · intro _ hx + simp at hx + · unfold SurjOn + simp end Set \ No newline at end of file diff --git a/Common/Set/Function.lean b/Common/Set/Function.lean new file mode 100644 index 0000000..f3ff153 --- /dev/null +++ b/Common/Set/Function.lean @@ -0,0 +1,235 @@ +import Mathlib.Data.Set.Function + +/-! # Common.Set.Function + +Additional theorems around functions defined on sets. +-/ + +namespace Set + +/-- +Produce a new function that swaps the outputs of the two specified inputs. +-/ +def swap [DecidableEq α] (f : α → β) (x₁ x₂ : α) (x : α) : β := + if x = x₁ then f x₂ else + if x = x₂ then f x₁ else + f x + +/-- +Swapping the same input yields the original function. +-/ +@[simp] +theorem swap_eq_eq_self [DecidableEq α] {f : α → β} {x : α} + : swap f x x = f := by + refine funext ?_ + intro y + unfold swap + by_cases hy : y = x + · rw [if_pos hy, hy] + · rw [if_neg hy, if_neg hy] + +/-- +Swapping a function twice yields the original function. +-/ +@[simp] +theorem swap_swap_eq_self [DecidableEq α] {f : α → β} {x₁ x₂ : α} + : swap (swap f x₁ x₂) x₁ x₂ = f := by + refine funext ?_ + intro y + by_cases hc₁ : x₂ = x₁ + · rw [hc₁] + simp + rw [← Ne.def] at hc₁ + unfold swap + by_cases hc₂ : y = x₁ <;> + by_cases hc₃ : y = x₂ + · rw [if_pos hc₂, if_neg hc₁, if_pos rfl, ← hc₂] + · rw [if_pos hc₂, if_neg hc₁, if_pos rfl, ← hc₂] + · rw [if_neg hc₂, if_pos hc₃, if_pos rfl, ← hc₃] + · rw [if_neg hc₂, if_neg hc₃, if_neg hc₂, if_neg hc₃] + +/-- +If `f : A → B`, then a swapped variant of `f` also maps `A` into `B`. +-/ +theorem swap_MapsTo_self [DecidableEq α] + {A : Set α} {B : Set β} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : MapsTo f A B) + : MapsTo (swap f a₁ a₂) A B := by + intro x hx + unfold swap + by_cases hc₁ : x = a₁ <;> by_cases hc₂ : x = a₂ + · rw [if_pos hc₁] + exact hf ha₂ + · rw [if_pos hc₁] + exact hf ha₂ + · rw [if_neg hc₁, if_pos hc₂] + exact hf ha₁ + · rw [if_neg hc₁, if_neg hc₂] + exact hf hx + +/-- +The converse of `swap_MapsTo_self`. +-/ +theorem self_MapsTo_swap [DecidableEq α] + {A : Set α} {B : Set β} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : MapsTo (swap f a₁ a₂) A B) + : MapsTo f A B := by + rw [← @swap_swap_eq_self _ _ _ f a₁ a₂] + exact swap_MapsTo_self ha₁ ha₂ hf + +/-- +If `f : A → B`, then `f` maps `A` into `B` **iff** a swap of `f` maps `A` into +`B`. +-/ +theorem self_iff_swap_MapsTo [DecidableEq α] + {A : Set α} {B : Set β} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) + : MapsTo (swap f a₁ a₂) A B ↔ MapsTo f A B := + ⟨self_MapsTo_swap ha₁ ha₂, swap_MapsTo_self ha₁ ha₂⟩ + +/-- +If `f : A → B` is one-to-one, then a swapped variant of `f` is also one-to-one. +-/ +theorem swap_InjOn_self [DecidableEq α] + {A : Set α} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : InjOn f A) + : InjOn (swap f a₁ a₂) A := by + intro x₁ hx₁ x₂ hx₂ h + unfold swap at h + by_cases hc₁ : x₁ = a₁ <;> + by_cases hc₂ : x₁ = a₂ <;> + by_cases hc₃ : x₂ = a₁ <;> + by_cases hc₄ : x₂ = a₂ + · rw [hc₁, hc₃] + · rw [hc₁, hc₃] + · rw [hc₂, hc₄] + · rw [if_pos hc₁, if_neg hc₃, if_neg hc₄, ← hc₂] at h + exact hf hx₁ hx₂ h + · rw [hc₁, hc₃] + · rw [hc₁, hc₃] + · rw [if_pos hc₁, if_neg hc₃, if_pos hc₄, ← hc₁, ← hc₄] at h + exact hf hx₁ hx₂ h.symm + · rw [if_pos hc₁, if_neg hc₃, if_neg hc₄] at h + exact absurd (hf hx₂ ha₂ h.symm) hc₄ + · rw [hc₂, hc₄] + · rw [if_neg hc₁, if_pos hc₂, if_pos hc₃, ← hc₂, ← hc₃] at h + exact hf hx₁ hx₂ h.symm + · rw [hc₂, hc₄] + · rw [if_neg hc₁, if_pos hc₂, if_neg hc₃, if_neg hc₄] at h + exact absurd (hf hx₂ ha₁ h.symm) hc₃ + · rw [if_neg hc₁, if_neg hc₂, if_pos hc₃, ← hc₄] at h + exact hf hx₁ hx₂ h + · rw [if_neg hc₁, if_neg hc₂, if_pos hc₃] at h + exact absurd (hf hx₁ ha₂ h) hc₂ + · rw [if_neg hc₁, if_neg hc₂, if_neg hc₃, if_pos hc₄] at h + exact absurd (hf hx₁ ha₁ h) hc₁ + · rw [if_neg hc₁, if_neg hc₂, if_neg hc₃, if_neg hc₄] at h + exact hf hx₁ hx₂ h + +/-- +The converse of `swap_InjOn_self`. +-/ +theorem self_InjOn_swap [DecidableEq α] + {A : Set α} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : InjOn (swap f a₁ a₂) A) + : InjOn f A := by + rw [← @swap_swap_eq_self _ _ _ f a₁ a₂] + exact swap_InjOn_self ha₁ ha₂ hf + +/-- +If `f : A → B`, then `f` is one-to-one **iff** a swap of `f` is one-to-one. +-/ +theorem self_iff_swap_InjOn [DecidableEq α] + {A : Set α} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) + : InjOn (swap f a₁ a₂) A ↔ InjOn f A := + ⟨self_InjOn_swap ha₁ ha₂, swap_InjOn_self ha₁ ha₂⟩ + +/-- +If `f : A → B` is onto, then a swapped variant of `f` is also onto. +-/ +theorem swap_SurjOn_self [DecidableEq α] + {A : Set α} {B : Set β} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : SurjOn f A B) + : SurjOn (swap f a₁ a₂) A B := by + show ∀ x, x ∈ B → ∃ a ∈ A, swap f a₁ a₂ a = x + intro x hx + have ⟨a, ha⟩ := hf hx + by_cases hc₁ : a = a₁ + · refine ⟨a₂, ha₂, ?_⟩ + unfold swap + by_cases hc₂ : a₁ = a₂ + · rw [if_pos hc₂.symm, ← hc₂, ← hc₁] + exact ha.right + · rw [← Ne.def] at hc₂ + rw [if_neg hc₂.symm, if_pos rfl, ← hc₁] + exact ha.right + · by_cases hc₂ : a = a₂ + · unfold swap + refine ⟨a₁, ha₁, ?_⟩ + rw [if_pos rfl, ← hc₂] + exact ha.right + · refine ⟨a, ha.left, ?_⟩ + unfold swap + rw [if_neg hc₁, if_neg hc₂] + exact ha.right + +/-- +The converse of `swap_SurjOn_self`. +-/ +theorem self_SurjOn_swap [DecidableEq α] + {A : Set α} {B : Set β} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : SurjOn (swap f a₁ a₂) A B) + : SurjOn f A B := by + rw [← @swap_swap_eq_self _ _ _ f a₁ a₂] + exact swap_SurjOn_self ha₁ ha₂ hf + +/-- +If `f : A → B`, then `f` is onto **iff** a swap of `f` is onto. +-/ +theorem self_iff_swap_SurjOn [DecidableEq α] + {A : Set α} {B : Set β} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) + : SurjOn (swap f a₁ a₂) A B ↔ SurjOn f A B := + ⟨self_SurjOn_swap ha₁ ha₂, swap_SurjOn_self ha₁ ha₂⟩ + +/-- +If `f : A → B` is a one-to-one correspondence, then a swapped variant of `f` is +also a one-to-one correspondence. +-/ +theorem swap_BijOn_self [DecidableEq α] + {A : Set α} {B : Set β} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : BijOn f A B) + : BijOn (swap f a₁ a₂) A B := by + have ⟨hf₁, hf₂, hf₃⟩ := hf + exact ⟨ + swap_MapsTo_self ha₁ ha₂ hf₁, + swap_InjOn_self ha₁ ha₂ hf₂, + swap_SurjOn_self ha₁ ha₂ hf₃ + ⟩ + +/-- +The converse of `swap_BijOn_self`. +-/ +theorem self_BijOn_swap [DecidableEq α] + {A : Set α} {B : Set β} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (hf : BijOn (swap f a₁ a₂) A B) + : BijOn f A B := by + have ⟨hf₁, hf₂, hf₃⟩ := hf + exact ⟨ + self_MapsTo_swap ha₁ ha₂ hf₁, + self_InjOn_swap ha₁ ha₂ hf₂, + self_SurjOn_swap ha₁ ha₂ hf₃ + ⟩ + +/-- +If `f : A → B`, `f` is a one-to-one correspondence **iff** a swap of `f` is a +one-to-one correspondence. +-/ +theorem self_iff_swap_BijOn [DecidableEq α] + {A : Set α} {B : Set β} {f : α → β} + (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) + : BijOn (swap f a₁ a₂) A B ↔ BijOn f A B := + ⟨self_BijOn_swap ha₁ ha₂, swap_BijOn_self ha₁ ha₂⟩ + +end Set diff --git a/Common/Set/Intervals.lean b/Common/Set/Intervals.lean index 433e288..505d65c 100644 --- a/Common/Set/Intervals.lean +++ b/Common/Set/Intervals.lean @@ -1,4 +1,5 @@ import Common.Logic.Basic +import Mathlib.Data.Set.Function import Mathlib.Data.Set.Intervals.Basic namespace Set @@ -8,6 +9,9 @@ namespace Set Additional theorems around intervals. -/ +/-- +If `m < n` then `{0, …, m - 1} ⊂ {0, …, n - 1}`. +-/ theorem Iio_nat_lt_ssubset {m n : ℕ} (h : m < n) : Iio m ⊂ Iio n := by rw [ssubset_def] @@ -22,4 +26,22 @@ theorem Iio_nat_lt_ssubset {m n : ℕ} (h : m < n) simp only [not_forall, not_lt, exists_prop] exact ⟨m, h, by simp⟩ +/-- +It is never the case that the emptyset is surjective +-/ +theorem SurjOn_emptyset_Iio_iff_eq_zero {n : ℕ} {f : α → ℕ} + : SurjOn f ∅ (Set.Iio n) ↔ n = 0 := by + apply Iff.intro + · intro h + unfold SurjOn at h + rw [subset_def] at h + simp only [mem_Iio, image_empty, mem_empty_iff_false] at h + by_contra nh + exact h 0 (Nat.pos_of_ne_zero nh) + · intro hn + unfold SurjOn + rw [hn, subset_def] + intro x hx + exact absurd hx (Nat.not_lt_zero x) + end Set \ No newline at end of file