From 2dff3f5794d89e632e386fe530c1cc34a3918856 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sun, 4 Jun 2023 17:34:42 -0600 Subject: [PATCH] Enderton. Chapter 2 exercises, 11-25. --- Bookshelf/Enderton/Set.tex | 401 ++++++++++++++++-- Bookshelf/Enderton/Set/Chapter_2.lean | 288 +++++++++++-- .../Enderton/Set/images/venn-diagram.png | Bin 0 -> 52225 bytes Common/Logic/Basic.lean | 17 +- Common/Set/Basic.lean | 23 +- 5 files changed, 663 insertions(+), 66 deletions(-) create mode 100644 Bookshelf/Enderton/Set/images/venn-diagram.png diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index cbe9530..dc9a457 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -1,5 +1,8 @@ \documentclass{report} +\usepackage{graphicx} +\graphicspath{{./Set/images/}} + \input{../../preamble} \makeleancommands{../..} @@ -1720,7 +1723,7 @@ Show that $A + (B + C) = (A + B) + C$. \end{proof} -\subsection{\unverified{Exercise 4.16}}% +\subsection{\verified{Exercise 4.16}}% \label{sub:exercise-4.16} Simplify: @@ -1728,11 +1731,26 @@ Simplify: \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_16} + + Let $A$, $B$, and $C$ be arbitrary sets. + Then + \begin{align*} + [(A \cup B \cup C) \cap (A \cup B)] & - [(A \cup (B - C)) \cap A] \\ + & = [A \cup B] - [A] \\ + & = \{ x \mid x \in (A \cup B) \land x \not\in A \} \\ + & = \{ x \mid x \in \{ y \mid y \in A \lor y \in B \} \land x \not\in A \} \\ + & = \{ x \mid (x \in A \lor x \in B) \land x \not\in A \} \\\ + & = \{ x \mid (x \in A \land x \not\in A) \lor (x \in B \land x \not\in A) \} \\ + & = \{ x \mid F \lor (X \in B \land x \not\in A) \} \\ + & = \{ x \mid x \in B \land x \not\in A \} \\ + & = B - A. + \end{align*} \end{proof} -\subsection{\unverified{Exercise 4.17}}% +\subsection{\verified{Exercise 4.17}}% \label{sub:exercise-4.17} Show that the following four conditions are equivalent. @@ -1746,11 +1764,58 @@ Show that the following four conditions are equivalent. \begin{proof} - TODO + \statementpadding + + \lean*{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_17\_i} + + \lean*{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_17\_ii} + + \lean*{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_17\_iii} + + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_17\_iv} + + Let $A$ and $B$ be arbitrary sets. + We show that (i) $(a) \Rightarrow (b)$, (ii) $(b) \Rightarrow (c)$, (iii) + $(c) \Rightarrow (d)$, and (iv) $(d) \Rightarrow (a)$. + + \paragraph{(i)}% + + Suppose $A \subseteq B$. + That is, $\forall t, t \in A \Rightarrow t \in B$. + Then there is no element such that $t \in A$ and $t \not\in B$. + By definition of the relative complement, this immediately implies + $A - B = \emptyset$. + + \paragraph{(ii)}% + + Suppose $A - B = \emptyset$. + By definition of the relative complement, + $$A - B = \emptyset = \{ x \mid x \in A \land x \not\in B \}.$$ + Then, for all $t$, + $\neg(t \in A \land t \not\in B) = t \not\in A \lor t \in B$. + This implies, by definition of the subset, that $A \subseteq B$. + It then immediately follows that $A \cup B = B$. + + \paragraph{(iii)}% + + Suppose $A \cup B = B$. + Then there is no member of $A$ that is not a member of $B$. + In other words, $A \subseteq B$. + This immediately implies $A \cap B = A$. + + \paragraph{(iv)}% + + Suppose $A \cap B = A$. + Then every member of $A$ is a member of $B$. + This immediately implies $A \subseteq B$. \end{proof} -\subsection{\unverified{Exercise 4.18}}% +\subsection{\partial{Exercise 4.18}}% \label{sub:exercise-4.18} Assume that $A$ and $B$ are subsets of $S$. @@ -1759,11 +1824,30 @@ List all of the different sets that can be made from these three by use of the \begin{proof} - TODO + We can reason about this diagrammatically: + + \begin{figure}[ht] + \includegraphics[width=0.6\textwidth]{venn-diagram} + \centering + \end{figure} + + In the above diagram, we assume the left circle corresponds to set $A$ and the + right circle corresponds to $B$. + The the possible sets we can make via the specified operators are: + + \begin{itemize} + \item $A - B$, the left circle excluding the overlapping region. + \item $A \cap B$, the overlapping region. + \item $B - A$, the right circle excluding the overlapping region. + \item $(A \cup B) \cap A$, the left circle. + \item $(A \cup B) \cap B$, the right circle. + \item $(A - B) \cup (B - A)$, the symmetric difference. + \item $A \cup B$, the entire diagram. + \end{itemize} \end{proof} -\subsection{\unverified{Exercise 4.19}}% +\subsection{\verified{Exercise 4.19}}% \label{sub:exercise-4.19} Is $\powerset{(A - B)}$ always equal to $\powerset{A} - \powerset{B}$? @@ -1771,11 +1855,35 @@ Is it ever equal to $\powerset{A} - \powerset{B}$? \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_19} + + Let $A$ and $B$ be arbitrary sets. + We show (i) that $\emptyset \in \powerset{(A - B})$ and (ii) + $\emptyset \not\in \powerset{A} - \powerset{B}$. + + \paragraph{(i)}% + \label{par:exercise-4.19-i} + + By definition of the \nameref{ref:power-set}, + $$\powerset{(A - B)} = \{ x \mid x \subseteq A - B \}.$$ + But $\emptyset$ is a subset of \textit{every} set. + Thus $\emptyset \in \powerset{(A - B)}$. + + \paragraph{(ii)}% + + By the same reasoning found in \nameref{par:exercise-4.19-i}, + $\emptyset \in \powerset{A}$ and $\emptyset \in \powerset{B}$. + But then, by definition of the relative complement, + $\emptyset \not\in \powerset{A} - \powerset{B}$. + + \paragraph{Conclusion}% + + By the \nameref{ref:extensionality-axiom}, the two sets are never equal. \end{proof} -\subsection{\unverified{Exercise 4.20}}% +\subsection{\verified{Exercise 4.20}}% \label{sub:exercise-4.20} Let $A$, $B$, and $C$ be sets such that $A \cup B = A \cup C$ and @@ -1784,22 +1892,95 @@ Show that $B = C$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_20} + + Let $A$, $B$, and $C$ be arbitrary sets. + By the \nameref{ref:extensionality-axiom}, $B = C$ if and only if for all sets + $x$, $x \in B \iff x \in C$. + We prove both directions of this biconditional. + + \paragraph{($\Rightarrow$)}% + + Suppose $x \in B$. + Then there are two cases to consider: + + \subparagraph{Case 1}% + + Assume $x \in A$. + Then $x \in A \cap B$. + By hypothesis, $A \cap B = A \cap C$. + Thus $x \in A \cap C$ immediately implying $x \in C$. + + \subparagraph{Case 2}% + + Assume $x \not\in A$. + Then $x \in A \cup B$. + By hypothesis, $A \cup B = A \cup C$. + Thus $x \in A \cup C$. + Since $x \not\in A$, it follows $x \in C$. + + \paragraph{($\Leftarrow$)}% + + Suppose $x \in C$. + Then there are two cases to consider: + + \subparagraph{Case 1}% + + Assume $x \in A$. + Then $x \in A \cap C$. + By hypothesis, $A \cap B = A \cap C$. + Thus $x \in A \cap B$, immediately implying $x \in B$. + + \subparagraph{Case 2}% + + Assume $x \not\in A$. + Then $x \in A \cup C$. + By hypothesis, $A \cup B = A \cup C$. + Thus $x \in A \cup B$. + Since $x \not\in A$, it follows $x \in B$. \end{proof} -\subsection{\unverified{Exercise 4.21}}% +\subsection{\verified{Exercise 4.21}}% \label{sub:exercise-4.21} Show that $\bigcup (A \cup B) = \bigcup A \cup \bigcup B$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_21} + + Let $A$ and $B$ be arbitrary sets. + By the \nameref{ref:extensionality-axiom}, the specified equality holds if and + only if for all sets $x$, + $$x \in \bigcup (A \cup B) \iff x \in \bigcup A \cup \bigcup B.$$ + We prove both directions of this biconditional. + + \paragraph{($\Rightarrow$)}% + + Suppose $x \in \bigcup (A \cup B)$. + By definition of the union of sets, there exists some $b \in A \cup B$ such + that $x \in b$. + If $b \in A$, then $x \in \bigcup A$ and $x \in \bigcup A \cup \bigcup B$. + Alternatively, if $b \in B$, then $x \in \bigcup B$ and + $x \in \bigcup A \cup \bigcup B$. + Regardless, $x$ is in the target set. + + \paragraph{($\Leftarrow$)}% + + Suppose $x \in \bigcup A \cup \bigcup B$. + Then $x \in \bigcup A$ or $x \in \bigcup B$. + WLOG, suppose $x \in \bigcup A$. + By definition of the union of sets, there exists some $b \in A$ such that + $x \in b$. + But then $b \in A \cup B$ meaning $x$ is also a member of + $\bigcup (A \cup B)$. \end{proof} -\subsection{\unverified{Exercise 4.22}}% +\subsection{\verified{Exercise 4.22}}% \label{sub:exercise-4.22} Show that if $A$ and $B$ are nonempty sets, then @@ -1807,11 +1988,39 @@ Show that if $A$ and $B$ are nonempty sets, then \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_22} + + Let $A$ and $B$ be arbitrary, nonempty sets. + By the \nameref{ref:extensionality-axiom}, the specified equality holds if and + only if for all sets $x$, + \begin{equation} + \label{sub:exercise-4.22-eq1} + x \in \bigcap (A \cup B) \iff x \in \bigcap A \cap \bigcap B. + \end{equation} + We prove both directions of this biconditional. + + \paragraph{($\Rightarrow$)}% + + Suppose $x \in \bigcap (A \cup B)$. + Then for all $b \in A \cup B$, $x \in B$. + In other words, for every member $b_1$ of $A$ and every member $b_2$ of $B$, + $x$ is a member of both $b_1$ and $b_2$. + But that implies $x \in \bigcap A$ and $x \in \bigcap B$. + + \paragraph{($\Leftarrow$)}% + + Suppose $x \in \bigcap A \cap \bigcap B$. + That is, $x \in \bigcap A$ and $x \in \bigcap B$. + By definition of the intersection of sets, forall sets $b$, if $b \in A$, + then $x \in b$. + Likewise, if $b \in B$, then $x \in b$. + In other words, if $b$ is a member of either $A$ or $B$, $x \in b$. + That immediately implies $x \in \bigcap (A \cup B$. \end{proof} -\subsection{\unverified{Exercise 4.23}}% +\subsection{\partial{Exercise 4.23}}% \label{sub:exercise-4.23} Show that if $\mathscr{B}$ is nonempty, then @@ -1819,46 +2028,186 @@ Show that if $\mathscr{B}$ is nonempty, then \begin{proof} - TODO + Refer to \nameref{sub:general-distributive-laws}. \end{proof} -\subsection{\unverified{Exercise 4.24a}}% +\subsection{\verified{Exercise 4.24a}}% \label{sub:exercise-4.24a} Show that if $\mathscr{A}$ is nonempty, then - $\powerset{\bigcap A} = \bigcap\; \{\powerset{X} \mid X \in \mathscr{A} \}$. + $\powerset{\bigcap\mathscr{A}} = + \bigcap\; \{\powerset{X} \mid X \in \mathscr{A} \}$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_24a} + + Suppose $\mathscr{A}$ is a nonempty set. + Then $\bigcap \mathscr{A}$ is well-defined. + Therefore + \begin{align*} + \powerset{\bigcap\mathscr{A}} + & = \{ x \mid x \subseteq \bigcap \mathscr{A} \} + & \textref{ref:power-set} \\ + & = \{ x \mid x \subseteq + \{ y \mid \forall X \in \mathscr{A}, y \in X \} \} + & \text{def'n intersection} \\ + & = \{ x \mid \forall t \in x, + t \in \{ y \mid \forall X \in \mathscr{A}, y \in X \} \} + & \text{def'n subset} \\ + & = \{ x \mid \forall t \in x, + (\forall X \in \mathscr{A}, t \in X) \} \\ + & = \{ x \mid \forall X \in \mathscr{A}, + (\forall t \in x, t \in X) \} \\ + & = \{ x \mid \forall X \in \mathscr{A}, x \subseteq X \} \\ + & = \{ x \mid \forall X \in \mathscr{A}, x \in \powerset{X} \} + & \textref{ref:power-set-axiom} \\ + & = \{ x \mid + \forall t \in \{ \powerset{X} \mid X \in \mathscr{A} \}, x \in t \} \\ + & = \bigcap\; \{\powerset{X} \mid X \in \mathscr{A}\}. + \end{align*} \end{proof} -\subsection{\unverified{Exercise 4.24b}}% +\subsection{\verified{Exercise 4.24b}}% \label{sub:exercise-4.24b} Show that - $$\bigcup\; \{ \powerset{X} \mid X \in \mathscr{A} \} \subseteq - \powerset{\bigcup A}.$$ + \begin{equation} + \label{sub:exercise-4.24b-eq1} + \bigcup\; \{ \powerset{X} \mid X \in \mathscr{A} \} \subseteq + \powerset{\bigcup\mathscr{A}}. + \end{equation} Under what conditions does equality hold? \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_24b} + + We first prove \eqref{sub:exercise-4.24b-eq1}. + Let $x \in \bigcup\; \{ \powerset{X} \mid X \in \mathscr{A} \}$. + By definition of the union of sets, + $(\exists X \in \mathscr{A}), x \in \powerset{X}$. + By definition of the \nameref{ref:power-set}, $x \subseteq X$. + By \nameref{sub:exercise-3.3}, $X \subseteq \bigcup \mathscr{A}$. + Therefore $x \subseteq \bigcup \mathscr{A}$, proving + $x \in \powerset{\mathscr{A}}$ as expected. + + \suitdivider + + \noindent + We show $\powerset{\bigcup A} \subseteq + \bigcup\;\{ \powerset{X} \mid X \in \mathscr{A} \}$ if and only if + $\bigcup\mathscr{A} \in \mathscr{A}$. + + \paragraph{($\Rightarrow$)}% + + Suppose $\powerset{\bigcup\mathscr{A}} \subseteq + \bigcup\;\{ \powerset{X} \mid X \in \mathscr{A} \}$. + By definition of the \nameref{ref:power-set}, + $\bigcup\mathscr{A} \in \powerset{\bigcup\mathscr{A}}$. + By hypothesis, $\bigcup\mathscr{A} \in + \bigcup\;\{ \powerset{X} \mid X \in \mathscr{A} \}$. + By definition of the union of sets, there exists some $X \in \mathscr{A}$ + such that $\bigcup\mathscr{A} \in \powerset{X}$. + That is, $\bigcup\mathscr{A} \subseteq X$. + But $\bigcup\mathscr{A}$ cannot be a proper subset of $X$ since + $X \in \mathscr{A}$. + Thus $\bigcup\mathscr{A} = X$. + This proves $\bigcup\mathscr{A} \in + \bigcup\;\{ \powerset{X} \mid X \in \mathscr{A} \}$. + + \paragraph{($\Leftarrow$)}% + + Suppose $\bigcup\mathscr{A} \in A$. + Let $x \in \powerset{\bigcup\mathscr{A}}$. + Since $\bigcup\mathscr{A} \in \mathscr{A}$, it immediately follows that + $x \in \{\powerset{X} \mid X \in \mathscr{A}\}$. + + \paragraph{Conclusion}% + + Equality follows immediately from this fact in conjunction with the proof + of \eqref{sub:exercise-4.24b-eq1}. \end{proof} -\subsection{\unverified{Exercise 4.25}}% +\subsection{\verified{Exercise 4.25}}% \label{sub:exercise-4.25} Is $A \cup \bigcup \mathscr{B}$ always the same as - $\bigcup\; \{ A \cup X \mid X \in \mathscr{B} \}$? + $\bigcup\;\{ A \cup X \mid X \in \mathscr{B} \}$? If not, then under what conditions does equality hold? \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_4\_25} + + We prove that + \begin{equation} + \label{sub:exercise-4.25-eq1} + A \cup \bigcup \mathscr{B} = + \bigcup\;\{ A \cup X \mid X \in \mathscr{B} \} + \end{equation} + if and only if $A = \emptyset$ or $\mathscr{B} \neq \emptyset$. + We prove both directions of this biconditional. + + \paragraph{($\Rightarrow$)}% + + Suppose \eqref{sub:exercise-4.25-eq1} holds true. + There are two cases to consider: + + \subparagraph{Case 1}% + + Suppose $B \neq \emptyset$. + Then $A = \emptyset \lor \mathscr{B} \neq \emptyset$ holds trivially. + + \subparagraph{Case 2}% + + Suppose $B = \emptyset$. + Then $$A \cup \bigcup \mathscr{B} = A \cup \bigcup \emptyset = A$$ and + $$ + \bigcup\;\{ A \cup X \mid X \in \mathscr{B} \} + = \bigcup \emptyset \\ + = \emptyset. + $$ + Then by hypothesis \eqref{sub:exercise-4.25-eq1}, $A = \emptyset$. + Then $A = \emptyset \lor \mathscr{B} \neq \emptyset$ holds trivially. + + \paragraph{($\Leftarrow$)}% + + Suppose $A = \emptyset$ or $\mathscr{B} \neq \emptyset$. + There are two cases to consider: + + \paragraph{Case 1}% + + Suppose $A = \emptyset$. + Then $A \cup \bigcup \mathscr{B} = \bigcup{\mathscr{B}}$. + Likewise, + $$ + \bigcup \{ A \cup X \mid X \in \mathscr{B} \} + = \bigcup \{ X \mid X \in \mathscr{B} \} \\ + = \bigcup \mathscr{B}. + $$ + Therefore \eqref{sub:exercise-4.25-eq1} holds. + + \paragraph{Case 2}% + + Suppose $B \neq \emptyset$. + Then + \begin{align*} + A \cup \bigcup\mathscr{B} + & = \{ x \mid x \in A \lor x \in \bigcup\mathscr{B} \} \\ + & = \{ x \mid x \in A \lor (\exists b \in \mathscr{B}) x \in b \} \\ + & = \{ x \mid (\exists b \in \mathscr{B}) x \in A \lor x \in b \} \\ + & = \{ x \mid (\exists b \in \mathscr{B}) x \in A \cup b \} \\ + & = \{ x \mid x \in \bigcup \{ A \cup X \mid X \in \mathscr{B} \} \\ + & = \bigcup \{ A \cup X \mid X \in \mathscr{B} \}. + \end{align*} + Therefore \eqref{sub:exercise-4.25-eq1} holds. \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean index 2290fd4..79edd4a 100644 --- a/Bookshelf/Enderton/Set/Chapter_2.lean +++ b/Bookshelf/Enderton/Set/Chapter_2.lean @@ -105,8 +105,6 @@ theorem exercise_3_4 (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B := by Assume that every member of `𝓐` is a subset of `B`. Show that `⋃ 𝓐 ⊆ B`. -/ theorem exercise_3_5 (h : ∀ x ∈ 𝓐, x ⊆ B) : ⋃₀ 𝓐 ⊆ B := by - unfold Set.sUnion sSup Set.instSupSetSet - simp only show ∀ y ∈ { a | ∃ t, t ∈ 𝓐 ∧ a ∈ t }, y ∈ B intro y hy rw [Set.mem_setOf_eq] at hy @@ -117,9 +115,8 @@ theorem exercise_3_5 (h : ∀ x ∈ 𝓐, x ⊆ B) : ⋃₀ 𝓐 ⊆ B := by Show that for any set `A`, `⋃ 𝓟 A = A`. -/ -theorem exercise_3_6a : ⋃₀ (Set.powerset A) = A := by - unfold Set.sUnion sSup Set.instSupSetSet Set.powerset - simp only +theorem exercise_3_6a : ⋃₀ (𝒫 A) = A := by + show { a | ∃ t, t ∈ { t | t ⊆ A } ∧ a ∈ t } = A ext x apply Iff.intro · intro hx @@ -136,11 +133,10 @@ theorem exercise_3_6a : ⋃₀ (Set.powerset A) = A := by Show that `A ⊆ 𝓟 ⋃ A`. Under what conditions does equality hold? -/ theorem exercise_3_6b - : A ⊆ Set.powerset (⋃₀ A) - ∧ (A = Set.powerset (⋃₀ A) ↔ ∃ B, A = Set.powerset B) := by + : A ⊆ 𝒫 (⋃₀ A) + ∧ (A = 𝒫 (⋃₀ A) ↔ ∃ B, A = 𝒫 B) := by apply And.intro - · unfold Set.powerset - show ∀ x ∈ A, x ∈ { t | t ⊆ ⋃₀ A } + · show ∀ x ∈ A, x ∈ { t | t ⊆ ⋃₀ A } intro x hx rw [Set.mem_setOf] exact exercise_3_3 x hx @@ -156,10 +152,8 @@ theorem exercise_3_6b Show that for any sets `A` and `B`, `𝓟 A ∩ 𝓟 B = 𝓟 (A ∩ B)`. -/ theorem exercise_3_7A - : Set.powerset A ∩ Set.powerset B = Set.powerset (A ∩ B) := by - suffices - Set.powerset A ∩ Set.powerset B ⊆ Set.powerset (A ∩ B) ∧ - Set.powerset (A ∩ B) ⊆ Set.powerset A ∩ Set.powerset B from + : 𝒫 A ∩ 𝒫 B = 𝒫 (A ∩ B) := by + suffices 𝒫 A ∩ 𝒫 B ⊆ 𝒫 (A ∩ B) ∧ 𝒫 (A ∩ B) ⊆ 𝒫 A ∩ 𝒫 B from subset_antisymm this.left this.right apply And.intro · unfold Set.powerset @@ -178,7 +172,7 @@ theorem exercise_3_7A Show that `𝓟 A ∪ 𝓟 B ⊆ 𝓟 (A ∪ B)`. -/ theorem exercise_3_7b_i - : Set.powerset A ∪ Set.powerset B ⊆ Set.powerset (A ∪ B) := by + : 𝒫 A ∪ 𝒫 B ⊆ 𝒫 (A ∪ B) := by unfold Set.powerset intro x hx simp at hx @@ -195,7 +189,7 @@ theorem exercise_3_7b_i Under what conditions does `𝓟 A ∪ 𝓟 B = 𝓟 (A ∪ B)`.? -/ theorem exercise_3_7b_ii - : Set.powerset A ∪ Set.powerset B = Set.powerset (A ∪ B) ↔ A ⊆ B ∨ B ⊆ A := by + : 𝒫 A ∪ 𝒫 B = 𝒫 (A ∪ B) ↔ A ⊆ B ∨ B ⊆ A := by unfold Set.powerset apply Iff.intro · intro h @@ -247,15 +241,15 @@ theorem exercise_3_7b_ii Give an example of sets `a` and `B` for which `a ∈ B` but `𝓟 a ∉ 𝓟 B`. -/ theorem exercise_3_9 (ha : a = {1}) (hB : B = {{1}}) - : a ∈ B ∧ Set.powerset a ∉ Set.powerset B := by + : a ∈ B ∧ 𝒫 a ∉ 𝒫 B := by apply And.intro · rw [ha, hB] simp · intro h - have h₁ : Set.powerset a = {∅, {1}} := by + have h₁ : 𝒫 a = {∅, {1}} := by rw [ha] exact Set.powerset_singleton 1 - have h₂ : Set.powerset B = {∅, {{1}}} := by + have h₂ : 𝒫 B = {∅, {{1}}} := by rw [hB] exact Set.powerset_singleton {1} rw [h₁, h₂] at h @@ -275,7 +269,7 @@ theorem exercise_3_9 (ha : a = {1}) (hB : B = {{1}}) Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`. -/ theorem exercise_3_10 (ha : a ∈ B) - : Set.powerset a ∈ Set.powerset (Set.powerset (⋃₀ B)) := by + : 𝒫 a ∈ 𝒫 (𝒫 (⋃₀ B)) := by have h₁ := exercise_3_3 a ha have h₂ := Chapter_1.exercise_1_3 h₁ generalize hb : 𝒫 (⋃₀ B) = b @@ -289,11 +283,7 @@ Show that for any sets `A` and `B`, `A = (A ∩ B) ∪ (A - B)`. -/ theorem exercise_4_11_i {A B : Set α} : A = (A ∩ B) ∪ (A \ B) := by - unfold Union.union Set.instUnionSet Set.union - unfold SDiff.sdiff Set.instSDiffSet Set.diff - unfold Inter.inter Set.instInterSet Set.inter - unfold Membership.mem Set.instMembershipSet Set.Mem setOf - simp only + show A = fun a => A a ∧ B a ∨ A a ∧ ¬B a suffices ∀ x, (A x ∧ (B x ∨ ¬B x)) = A x by conv => rhs; ext x; rw [← and_or_left, this] intro x @@ -310,10 +300,7 @@ Show that for any sets `A` and `B`, `A ∪ (B - A) = A ∪ B`. -/ theorem exercise_4_11_ii {A B : Set α} : A ∪ (B \ A) = A ∪ B := by - unfold Union.union Set.instUnionSet Set.union - unfold SDiff.sdiff Set.instSDiffSet Set.diff - unfold Membership.mem Set.instMembershipSet Set.Mem setOf - simp only + show (fun a => A a ∨ B a ∧ ¬A a) = fun a => A a ∨ B a suffices ∀ x, ((A x ∨ B x) ∧ (A x ∨ ¬A x)) = (A x ∨ B x) by conv => lhs; ext x; rw [or_and_left, this x] intro x @@ -418,4 +405,249 @@ theorem exercise_4_14 : A \ (B \ C) ≠ (A \ B) \ C := by end +/-- ### Exercise 4.16 + +Simplify: +`[(A ∪ B ∪ C) ∩ (A ∪ B)] - [(A ∪ (B - C)) ∩ A]` +-/ +theorem exercise_4_16 {A B C : Set α} + : ((A ∪ B ∪ C) ∩ (A ∪ B)) \ ((A ∪ (B \ C)) ∩ A) = B \ A := by + calc ((A ∪ B ∪ C) ∩ (A ∪ B)) \ ((A ∪ (B \ C)) ∩ A) + _ = (A ∪ B) \ ((A ∪ (B \ C)) ∩ A) := by rw [Set.union_inter_cancel_left] + _ = (A ∪ B) \ A := by rw [Set.union_inter_cancel_left] + _ = B \ A := by rw [Set.union_diff_left] + +/-! ### Exercise 4.17 + +Show that the following four conditions are equivalent. + +(a) `A ⊆ B` +(b) `A - B = ∅` +(c) `A ∪ B = B` +(d) `A ∩ B = A` +-/ + +theorem exercise_4_17_i {A B : Set α} (h : A ⊆ B) + : A \ B = ∅ := by + ext x + apply Iff.intro + · intro hx + exact absurd (h hx.left) hx.right + · intro hx + exact False.elim hx + +theorem exercise_4_17_ii {A B : Set α} (h : A \ B = ∅) + : A ∪ B = B := by + suffices A ⊆ B from Set.left_subset_union_eq_self this + show ∀ t, t ∈ A → t ∈ B + intro t ht + rw [Set.ext_iff] at h + by_contra nt + exact (h t).mp ⟨ht, nt⟩ + +theorem exercise_4_17_iii {A B : Set α} (h : A ∪ B = B) + : A ∩ B = A := by + suffices A ⊆ B from Set.inter_eq_left_iff_subset.mpr this + exact Set.union_eq_right_iff_subset.mp h + +theorem exercise_4_17_iv {A B : Set α} (h : A ∩ B = A) + : A ⊆ B := Set.inter_eq_left_iff_subset.mp h + +/-- ### Exercise 4.19 + +Is `𝒫 (A - B)` always equal to `𝒫 A - 𝒫 B`? Is it ever equal to `𝒫 A - 𝒫 B`? +-/ +theorem exercise_4_19 {A B : Set α} + : 𝒫 (A \ B) ≠ (𝒫 A) \ (𝒫 B) := by + intro h + have he : ∅ ∈ 𝒫 (A \ B) := by simp + have ne : ∅ ∉ (𝒫 A) \ (𝒫 B) := by simp + rw [Set.ext_iff] at h + have := h ∅ + exact absurd (this.mp he) ne + +/-- ### Exercise 4.20 + +Let `A`, `B`, and `C` be sets such that `A ∪ B = A ∪ C` and `A ∩ B = A ∩ C`. +Show that `B = C`. +-/ +theorem exercise_4_20 {A B C : Set α} + (hu : A ∪ B = A ∪ C) (hi : A ∩ B = A ∩ C) : B = C := by + ext x + apply Iff.intro + · intro hB + by_cases hA : x ∈ A + · have : x ∈ A ∩ B := Set.mem_inter hA hB + rw [hi] at this + exact this.right + · have : x ∈ A ∪ B := Set.mem_union_right A hB + rw [hu] at this + exact Or.elim this (absurd · hA) (by simp) + · intro hC + by_cases hA : x ∈ A + · have : x ∈ A ∩ C := Set.mem_inter hA hC + rw [← hi] at this + exact this.right + · have : x ∈ A ∪ C := Set.mem_union_right A hC + rw [← hu] at this + exact Or.elim this (absurd · hA) (by simp) + +/-- ### Exercise 4.21 + +Show that `⋃ (A ∪ B) = (⋃ A) ∪ (⋃ B)`. +-/ +theorem exercise_4_21 {A B : Set (Set α)} + : ⋃₀ (A ∪ B) = (⋃₀ A) ∪ (⋃₀ B) := by + ext x + apply Iff.intro + · intro hx + have ⟨t, ht⟩ : ∃ t, t ∈ A ∪ B ∧ x ∈ t := hx + apply Or.elim ht.left + · intro hA + exact Or.inl ⟨t, ⟨hA, ht.right⟩⟩ + · intro hB + exact Or.inr ⟨t, ⟨hB, ht.right⟩⟩ + · intro hx + apply Or.elim hx + · intro hA + have ⟨t, ht⟩ : ∃ t, t ∈ A ∧ x ∈ t := hA + exact ⟨t, ⟨Set.mem_union_left B ht.left, ht.right⟩⟩ + · intro hB + have ⟨t, ht⟩ : ∃ t, t ∈ B ∧ x ∈ t := hB + exact ⟨t, ⟨Set.mem_union_right A ht.left, ht.right⟩⟩ + +/-- ### Exercise 4.22 + +Show that if `A` and `B` are nonempty sets, then `⋂ (A ∪ B) = ⋂ A ∩ ⋂ B`. +-/ +theorem exercise_4_22 {A B : Set (Set α)} + : ⋂₀ (A ∪ B) = ⋂₀ A ∩ ⋂₀ B := by + ext x + apply Iff.intro + · intro hx + have : ∀ t : Set α, t ∈ A ∪ B → x ∈ t := hx + show (∀ t : Set α, t ∈ A → x ∈ t) ∧ (∀ t : Set α, t ∈ B → x ∈ t) + rw [← forall_and] + intro t + exact ⟨ + fun ht => this t (Set.mem_union_left B ht), + fun ht => this t (Set.mem_union_right A ht) + ⟩ + · intro hx + have : ∀ t : Set α, (t ∈ A → x ∈ t) ∧ (t ∈ B → x ∈ t) := by + have : (∀ t : Set α, t ∈ A → x ∈ t) ∧ (∀ t : Set α, t ∈ B → x ∈ t) := hx + rwa [← forall_and] at this + show ∀ (t : Set α), t ∈ A ∪ B → x ∈ t + intro t ht + apply Or.elim ht + · intro hA + exact (this t).left hA + · intro hB + exact (this t).right hB + +/-- ### Exercise 4.24a + +Show that is `𝓐` is nonempty, then `𝒫 (⋂ 𝓐) = ⋂ { 𝒫 X | X ∈ 𝓐 }`. +-/ +theorem exercise_4_24a {𝓐 : Set (Set α)} + : 𝒫 (⋂₀ 𝓐) = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := by + calc 𝒫 (⋂₀ 𝓐) + _ = { x | x ⊆ ⋂₀ 𝓐 } := rfl + _ = { x | x ⊆ { y | ∀ X, X ∈ 𝓐 → y ∈ X } } := rfl + _ = { x | ∀ t ∈ x, t ∈ { y | ∀ X, X ∈ 𝓐 → y ∈ X } } := rfl + _ = { x | ∀ t ∈ x, (∀ X, X ∈ 𝓐 → t ∈ X) } := rfl + _ = { x | ∀ X ∈ 𝓐, (∀ t, t ∈ x → t ∈ X) } := by + ext + rw [Set.mem_setOf, Set.mem_setOf, forall_mem_comm (· ∈ ·)] + _ = { x | ∀ X ∈ 𝓐, x ⊆ X} := rfl + _ = { x | ∀ X ∈ 𝓐, x ∈ 𝒫 X } := rfl + _ = { x | ∀ t ∈ { 𝒫 X | X ∈ 𝓐 }, x ∈ t} := by simp + _ = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := rfl + +/-- ### Exercise 4.24b + +Show that +``` +⋃ {𝒫 X | X ∈ 𝓐} ⊆ 𝒫 ⋃ 𝓐. +``` +Under what conditions does equality hold? +-/ +theorem exercise_4_24b {𝓐 : Set (Set α)} + : (⋃₀ { 𝒫 X | X ∈ 𝓐 } ⊆ 𝒫 ⋃₀ 𝓐) + ∧ ((⋃₀ { 𝒫 X | X ∈ 𝓐 } = 𝒫 ⋃₀ 𝓐) ↔ (⋃₀ 𝓐 ∈ 𝓐)) := by + have hS : (⋃₀ { 𝒫 X | X ∈ 𝓐 } ⊆ 𝒫 ⋃₀ 𝓐) := by + simp + exact exercise_3_3 + refine ⟨hS, ?_⟩ + apply Iff.intro + · intro rS + have rS : 𝒫 ⋃₀ 𝓐 ⊆ ⋃₀ { 𝒫 X | X ∈ 𝓐 } := + (Set.Subset.antisymm_iff.mp rS).right + have hA : ⋃₀ 𝓐 ∈ ⋃₀ { 𝒫 X | X ∈ 𝓐 } := + rS Set.self_mem_powerset_self + conv at hA => + rhs + unfold Set.sUnion sSup Set.instSupSetSet + simp only + have ⟨X, ⟨⟨x, hx⟩, ht⟩⟩ := Set.mem_setOf.mp hA + have : ⋃₀ 𝓐 = x := by + rw [← hx.right] at ht + have hl : ⋃₀ 𝓐 ⊆ x := ht + have hr : x ⊆ ⋃₀ 𝓐 := exercise_3_3 x hx.left + exact Set.Subset.antisymm hl hr + rw [← this] at hx + exact hx.left + · intro hA + suffices 𝒫 ⋃₀ 𝓐 ⊆ ⋃₀ { 𝒫 X | X ∈ 𝓐 } from + subset_antisymm hS this + show ∀ x, x ∈ 𝒫 ⋃₀ 𝓐 → x ∈ ⋃₀ { x | ∃ X, X ∈ 𝓐 ∧ 𝒫 X = x } + intro x hx + unfold Set.sUnion sSup Set.instSupSetSet + simp only [Set.mem_setOf_eq, exists_exists_and_eq_and, Set.mem_powerset_iff] + exact ⟨⋃₀ 𝓐, ⟨hA, hx⟩⟩ + +/-- ### Exercise 4.25 + +Is `A ∪ (⋃ 𝓑)` always the same as `⋃ { A ∪ X | X ∈ 𝓑 }`? If not, then under +what conditions does equality hold? +-/ +theorem exercise_4_25 {A : Set α} (𝓑 : Set (Set α)) + : (A ∪ (⋃₀ 𝓑) = ⋃₀ { A ∪ X | X ∈ 𝓑 }) ↔ (A = ∅ ∨ Set.Nonempty 𝓑) := by + apply Iff.intro + · intro h + by_cases h𝓑 : Set.Nonempty 𝓑 + · exact Or.inr h𝓑 + · have : 𝓑 = ∅ := Set.not_nonempty_iff_eq_empty.mp h𝓑 + rw [this] at h + simp at h + exact Or.inl h + · intro h + apply Or.elim h + · intro hA + rw [hA] + simp + · intro h𝓑 + calc A ∪ (⋃₀ 𝓑) + _ = { x | x ∈ A ∨ x ∈ ⋃₀ 𝓑} := rfl + _ = { x | x ∈ A ∨ (∃ b ∈ 𝓑, x ∈ b) } := rfl + _ = { x | ∃ b ∈ 𝓑, x ∈ A ∨ x ∈ b } := by + ext x + rw [Set.mem_setOf, Set.mem_setOf] + apply Iff.intro + · intro hx + apply Or.elim hx + · intro hA + have ⟨b, hb⟩ := Set.nonempty_def.mp h𝓑 + exact ⟨b, ⟨hb, Or.inl hA⟩⟩ + · intro ⟨b, hb⟩ + exact ⟨b, ⟨hb.left, Or.inr hb.right⟩⟩ + · intro ⟨b, ⟨hb, hx⟩⟩ + apply Or.elim hx + · exact (Or.inl ·) + · intro h + exact Or.inr ⟨b, ⟨hb, h⟩⟩ + _ = { x | ∃ b ∈ 𝓑, x ∈ A ∪ b } := rfl + _ = { x | ∃ t, t ∈ { y | ∃ X, X ∈ 𝓑 ∧ A ∪ X = y } ∧ x ∈ t } := by simp + _ = ⋃₀ { A ∪ X | X ∈ 𝓑 } := rfl + end Enderton.Set.Chapter_2 \ No newline at end of file diff --git a/Bookshelf/Enderton/Set/images/venn-diagram.png b/Bookshelf/Enderton/Set/images/venn-diagram.png new file mode 100644 index 0000000000000000000000000000000000000000..8e21612be3051d6519159279fb2bee12c068bdec GIT binary patch literal 52225 zcmeFZhd$Vxf(ELuWIRI+#WmT^u}Nh*7fqf)km z>|^{MmtLRG_xt-3ez)82b?be5^?s%2xt`bc829nG&O=>owF5M4G#Cu#fchn6eGG>D z3kI|IC^aSgm(;WB;qb40H!qpq#$cFv(ErHP^-s=YFvl?J$_j=)12eME{UjtoHo-U5Fy0rA$t6K|NZW0xY)nny!+oLME%c0um0~7)c)t8r~mf}|NGD* z|NDghedy!=dBXp{tpE1=|KF{D8}a|q*rI0)TKhp&>rG5jQB@uI(RknW@1Jj#J`1)9 zV)l;?u%G|Bu`=syS?g6%={jhZt{R!I8p&o7k6#1# zxq=*tb$_F_Ncf%Ftrq;Irf%R?Q}E{fdeU6&%4Bx3S(@@gA?#FF9JkuRhzAdf^)oe0 zGc}&il(ov1eTrl^C#}pDcoRp?U;9kYF5&k2TcT8NPobr=|H@3sS%>c?o}T40fg4>x zn+s~VP)ta*s>NPR9W$izsQAXT_0Emp?Z3&h>wm{r=6@*F-X4z{uJi3Iw0LXFB5GA$ z=FmC->ztivPxqQ1RT!-GE}9*B+j;oGb3x;QI^Vx8i(}2_Z9hHCb48NnpUa2c~}>I ze*9ZRzK>xonnyEkh8Q&2d+8Z(Waj0BmEeF$;$+iyyIc`L32!{Q+KpFweZgaMM{q&! zM5?u*-KWQKXC1V6-1!Z2o-hfUb!o&2P3}Z?=NVV|El-(tW?i0*5XBWI$@u%-I^#8C zLRuMgcb)9WtPI-n8^i_H&W_X%t`G^t<~~@;?9ybX*Y>8bPFtZh-mS`Qcu_9ep*5+$ zC0=w^Gl=ntjE0z`V+>;&)5@;MbRDw-kKlM;m(5 z)uN3#JY~+si&zdky9*oT$0Dg2Clq&Fi86Sir_uZ8hlkcOucw2b@m`*yTh`!=RVL^B zyqsyB?X&Q6Ti)vJE&H8i=k7Q5aOx#B*l9mCbG&y`6i4ui=02_Q?}=MK0^3p)MwWLb zwm3KHm;9$zjl>KyHJAjgadppy&3g`~?V+GCNs{&z@}3(Cx+T9O zEMSnev?GiCy-au`x)sbLutB^WFOq2gCAPWLzU7a4tTx9)uYQvi-nb=Bc#ELf{31py z(ZZzqW~%EzdGoVK*pI=xRCJped(|m0^t}(9F&Jn9^X$0^g>D5kl~W@lxWGZTq3R!& z!?(x3_dh($w`qeV-~u5P&YM@XO(W)RZBK5%1cq0po8-hl$MiW^DNj3O3&Txk%n zGjz>k-{X0U(x*y$eG zj?^>Ek!3kb1%zPuOC!z6=Ura~PZBiueTSb4TG8Y_Hr-QDCTw20mW$c)-dfTO){)Cf zPERIj;-iA-wyZ)4-W?h0=dXV~68za%KeJcm;r;D;Y^i)v^e4AdhB>3@r&Jy>mISOX zt_PRJQ1KknxDfQ}+T=1#-SrLs4G$jP(B4bB@#V#tG3%x zl}2)VKSyY*@*gsc-`?ILt&BAvCT)|5>e9Qr_dy(!0{wW+Ni0=a(T-Ow>ga+JX@rR<<8)|7#hs6 z!b2#y=N=(;xu7~eEPQCG*X+Q$067mU* zn{5J=TkHHKomQ;andRP%vUbNOpDfDx)OPB&wU(TxKHOo}5e)5I4V7Hd5IgrL?V850 zudrngJ{=dmTZN&N$WH(cIA%n0GPb0PoLbUOmL2Be?|ynk!orTn??U(YSo~~OUS3{1 zHP3zxq1dZkg_eVmE5A8xXXW(LQm71gXr}myeIYxUg%v`k zbRB+IuZ$b3>$n6sZcX|;@fyqdTa=*_@p$=a(FdKx0GXM*2(F3IJb%1RBc+b?^{+2} zJWSC(>u7N)IBP&4eXdqDd{3g^mhY6NrQeoJi82`XK(3&Eo*({a(O+HkbV`l#d!EI?H5CD;WM_@T2a25XLF{TsbE~Dq!uV^`E?i z>aMrljaibFQ(4Zvk7_0dSkv5U7-)Hp3|wTG=$lIJKFEZ1i5D{c*?bq0Gbx%&ZY2Zb zzS3&-@WChh*z(D9cipZU+{u=6p7m~zxrUv3e$LTT#nMmMs7E9*S;VTxdb-uTIWz8p zvwM_R$3$;O?*7Og{?vA2`bi}zoASSE!E-_;l=2pPVa1A6yDPSImg#e3pu1W_qAkPro04a>Dm=-gj=t8TUicAvP<~!$rK+m z!Rw5M>T}p)?Zvkl%%#TN6F&JZZA^Q9B=E*cE~m&`&^UK)CGDEs+|b+eZbKKi*l9c` zpIh8`tU{pE5b~T-gnh2SxzjM68Y5j}JLfp+?}OWz66A8|SiPrBKC#M^3$15&xoCrr z>(EX4T{Va|XukVNy8N~hZOC$Q&R`0!_Uj3f?5p#xQ&l&d#+1`}G&uKEX-z8VSsF+3 zPEd+kDirA*7XHw^Xv0IlvD{^O1!YW3*nG__dw5nTm;C_t9 z0VrqGA^K3AZE9G}p=*KFJ6J0jFcT+j(v3c=s zzo&+4t0FmN2L60Y822|WpD{@^-KrU2WjG?G%VIn{)K?vL;e3Fo)9cB(;o6Z*<6DPJ zf(p(s4j-+&+OQ|#w9TF6>E2cyy9vX4alGSSp0_+R&Uy<<%Aj3bBc{UDjihX*UUF9=I`f zQa$G6$dz8%gFJ@^8qz%WV%5ac(&lmsb*#%BpURznV^?IJd_=!atbl z=iQeVKH0PP2O;VJd0f}xvHQt~s|&QMDksbDYuk~3N-b}7fUXD27h#$8Y`=9)_=?eq zr#za>I$}%pxzD&v%dRgM)~RO24y{afHa$BW`N>iA34?XHb&cnwtzA>pav)piQw$HEycX|K zjq|bBCjPulPNEjDs;ef_&$0Sqxu(ZrFsy|g?jAObzdg~GI3_H`;{>+MpbznV> z=pd}$vs#5~eSTW7f%(BE}m0EjID;(bmX?WSUjCy-unIJd4baXgGpBfO?w!w^L&wfnMQuM{S?F}3W#NZ z2BQVCCW(^RsqQmDJe12*-DNR6ntlvVc`vgOi=E{nn3<+i-v9<0u}r>rJInjeUI-e< zI>V}GdCiCN_gMN0YvVkA-4mTNlCZS&9lj*tzv4n5>#TG&-wEnn4IIsQI6~!TJ)tVa z)4_)Cc<+WC>+UzU)jn|mJ|9wK^ERA>4>z4&%_$2ylHY@l?lFx$p1UncTkp1GV3_0mZGk+Or0Rgi2AEV{ACy0jvg9S~uH>QgM zO{?5WX&)EoaC7l#AH^?gbNC8x_T)rJE^2(Gliv5r<` z4LPF2TP~-<%|8{R1FaGu{%^I#mRNyb>S2-*l5s`f)3$3A!)b!1<0WSX{8OVc+!iH$ z7c+JwrTLE^&9y5$X-Xgr$YdA@Y~YN4$~b&~ZOpN*@%+?QbX35`(xlAWwnA>`AtX)W z*?K~`(0YHFLtQnLv}1*2?~0UD_rG(_oJ(bRARlj;&Rx^*+#JJm{^qDWqB{WoTe-rz zEPHV@*h3YKiu+U}n1x;Xift-g`o*jR^3O0!&ODe^e>I z!`DW~?$6;aI?NBuwGv`xy_qplSMN@$p2)0UJAXvX<9yRH+yJSg!r3@j&TXWw{{%O8 zVEdv2I8=cpI&4(zT69~>O~1c+iZkM`@n+B^FgPR^f+ zJ)!c*1h}sY5F$j4@$C`ALhsxUPka_6>y6@0G;taz&s9-Y_W4;@FFFvBv6{@_Q_qFp zT+|E>K6SkPfV~-G5OG9Clzd`q|1Qn&I3Vu=!qYoqT47?1H&ClZw~-9>X92z?oMv72 z#=SZuQ}~zuA(QWteoKyA#_dTDfrt6A=+ddoTqg^vl~=Qpii$Ov2(0j&)VIDflxx6e z&0Dydyn>ske{u2lb)5@0dh(qTrMxRWetlXmJi@~Q8*J-Bfxr!fApJDxS@U@lHr8~a zeiIJ>F0(%lD82v=8oU$X=?QJQza7b z({XK(63O@e&oTzl0p#VJEj+^*nc_&)Xibu-Z?USrX+!)oc?p2&@Z6OGGjZZZZeI59 zk5iO4cEYyTo1(eOl=eJOU=wf8JyK8bZ0!4SooUZA&{a$sIOaZW+@M_nSe-QJ-ohaV$YNUeOKnD@~& zlWaDoxPZ5WjqF3`gjJ%rT zmDU8Ad}1X?4{MjLYP6-G-UW46O1fUWH8zj$EwNLR!xdT{WHW#3IT>SJQt)eb#*yrO zge*I!w9nOeQR~XRR0sQ}y7OE?Z<2juRPTo+5HbQqH}q}wKr5MUOT8Pcdio85bm-`S zGCokDqnUc+CHUCja1z1R>xT$9jTt;F zd+OZCU!AeLCwlsdv1Q`fS;uzc&^;9SHjVdCVN4Krj^ks13|zH501=$ta`1!V#*8kX zWiporW2M{h4Ui81+A9D01j*8#hNHJ^dAjVI_CYZl+f_iQaE`ac2PJAt0~3Z{iZtP3 z$Fy<{3IheruIHC9@KAHBJ}!nv=$kFn=G1#v9$u~>khBs+Y6TS{fSdvoB+}3}{z#iB zWKrD)O46T}rv@397UU!s*c@181FDIB?QTZ`56bv1e$c__y@qZFzvNE?Ee&&O!-E<~ zw0bGyUx_7-4BzO=`H{}Yrly{7zJTbeH;(Fh5O*6YB*%XMFb~Q;kMn0Bzu_0T42`|~5uQVA zJbH>L;hARgl29J$7HeqCEmxvtH$Fp}%_-o4m7EXW4v_Nr8Ai0ggb+0R&CcCPvkjBg zIk%lv!ZaJ!;c7eeVft_O^>43MmV2#92XjHd^lMN`HWt#M`uA$ZsqkuK6l0`S;vhtY zbk6GB@ZgQ!LRXZrrz?l=PaIDWd#Sw|$i|LV$K`87CsmOs35n)22(|gRhJtyh4+x()i*l#V zETeprGjazDWoRzm{z#Q%CO?%2n z;V_I#&rGj5z8`ZZGKO|Gx#MAqJ8u0`(}dWy&!fq9MEnj;RIP{5>F{!;Zm8Phu8b&Z z*(eSq9zj{pV3cN3F0!h>!G0c6ColXH6xCH3>M0|@Kx-mlP%S`nYMGh;(a0HM4J4J8 z`q)Iyr8GyypEl2jmk}B-=eu zkv>mcsFc*FNg43gO;IYH{u_0jNvDQAa}G)K9A#_o+{eviQT_V~;9cm3XF_4y$h%bZCDf~YoN^Z) zv!31jT*=Iuw>Oi6iYEU`o>9edrF(rK?^EYs-bcyqtth(z%DPe6^~;36iwjL$q(YWi zU%j+c+ecmvLttyTbK0E|`?qc@J{tRX=2@AaB)tmUY8mzoM;QPZXi1W(rD}twiyv?* zc5FXESE;9`mlV?GN=2_-jz1+SIY28o@FPt|^xG@(GTV=j*2h!5OrG=Wy*I0Ja|JPa z(XD>v{k-WVuvp;Od&3o3=i_qBGh`@fl8~@_O)-&|LJRw{yhtToK-jE&URg1nUucV* z-ke{(8mt6iYupeN>FeOethRoX+g^x{JLjaIXH@X&0GI60%G~g@dU(w|o3Bk1?Z3C! zW`(G&k|!fV6|VGOb(3=&24W{@S+kU9j`!UALe&rqA_s&(uPLfkb!SqA^etY@J@F{6 z#(l8zo17q4Ox@CF_*hoa`*2!P!NVFE4{#a0wl=VCYX8FNog8`x%DZ+cgM~6eP&BLb z(pCE%k^`?pr}^uq4{l6dZ5Lo7xugP1umc92+`ETsyp;grX6#_M-p=OVRvGH+-(UB$_)l$2 ztjrD$#tIln^IO$;Hs3vg`QXK7-0m;|(%a@)!>R{PE}1~0M?!THB`YA45aS4Nv7a5N zNHTGh*za!zF$&;)-W)+46L^dCPB3j2-D+!8!JXRRvgEepDB$jy67iU3!EA~pT6G*` ziOhAJG}SW1ua`n4 zVwdqNC)`TEnk}LSq_O~z1}@?1hH{Vt80`OM0hT6%mL!YshiD&y4-C|vDqDs;MvZNH zu&T)W$L&8~CzA_mu9RpeN}flIu*xlwc=yN2!~c#v=m50J{kn=NZnezpf_f9ZMajRX0>z2RPj-V8*0F z&TeI7Aq2jg@6}aaHr}Tj{P{7$b@W~62)1{;K>MQ8(*U3lflVzN%hOwDgZS#etrFlnkpQ^%CgWmP}bGXLp2Gk_{C$53+TyEKTIgdTNDyPm*|KX~Iz|$pL=NSJ548$kiG-Yrb>`J^VO4||FUj8rs#QJed4&jS)0~L9M z{mA>>S;vG_DJ3@!q-KiLeWLpHF~R}a(umO`=*KOn7R|YQLeJ$W*MFs92PBz!c7f5? za={}#`KETr#JL&^M4B*|miY=*NZ`@^VEb({v(4@soj8lBli4_WP$&c1a2$4SsK1Ho z?DemXrlr>wD3(FtTI52=j_;U;5E39!a+T19i;Wu73~gh7e_=x2q39W-V;ydoz{wrK zO9dt+??IzzrlrIv@SZly`TZ9;iW!PhRi1ZWc-7~~pK~9P7G)F2rCuFu{I3e&0kQ|# zi=}>i0oH@w^}Cb@gn)_Q=;Uk7mwFMDhR*MQO#j^;40-%Jv1?3$IMSR{g0ydG#f|PS zt2G&y6MCc;YA)wn`BoY9IdjMCwn^%|mDPeV^r;ub$V=45hZE^28i{!t(-7QmJueHQ|L-u5?MVzR$8|2C|&u1YC%8<5& znf|lZR(SgsX1Ocf)gE>`0XpEjGo3R0{OX*OEg;BpaPIm+>QI!;g?+|&2*3WxMsEP2 zBB#VHput;cS$iGmU>UegrjHl}>IRdJDeS>N^6kpeOLE~~z+l1(L55oE`vMiA0My_( zF?$W-yQWC?-cwiJT;o=YD*x3KO`3e8yY+Rq#_vA<8G8I-6DX%PgH`TT0C-GMS{r0( z$wukd`FJ=3t^fAoOk@1@ky`I)?fsar3yH5f4iUbPb1 zGohF1#zTtTF#o~W8}b4;`&w}95q|lJBa2WOT-N4)#PR8HCeIo-$$(P9dF|Y4(ew*4 z%nueSPuj5(yCxR^yh(-=E2oDsFGVaRox5_LiYi5cw3Bh7k5*$h2*V95_Kq+@lJ2An zK8rqj(H81+2|`b&M`;k?B|f|dbaP|mh(0jhCay9q(ki5toutS5CEpWo;Yzr z2nrW&JQLm*x2hsnXwHq_+4hHW2q6=8h{pcG@*a*=&3KXZiHCPopy|xux2N$!L7Qtv zCAKQoe)(K{Pcb2V+{J`U(ALoih5vY>_sm^7+4=C#pl?-zdc2;Kwh|0D7C_T6XC025GrPk5A1+nXQ zA!MA~u_igR)&Sk6hu)S618dZNec^|MGQ+>8FX^GDyVbg3&@2dcs;l|d_;*(XeS;@= zrio735kUuAgvpM1@iC)t>@*!9E+U0x03ZtV*iMLIg+r9T@KJo!HC^|fi5l&xiZ*?kG?mg4OHQhdy*5YM8Yc1a|rp>=_gS2T|kSigmy@Zyb5%59>PQU|x1T5_0m};fNPA?+?Rfqkz7ufS!MS0eI$U zB9@1qD`+j%d+4nFmuuER>zS~+Z_&(qG4swb5%8&fup2T@byv4^f;XOd|H7~Rq#dmH zuOjfXKC68P^)KY+BWL;I6y1Bp+4aH$&866BBX((@V(5F{#);TkP2@zNx(0>?muCBY zISgj!f#ehn7A=3UfuRb-3kk%uzO^QYEN%pd)Mm-RgZ3^OY&e)8G0W zpel{{j&mf}i^5nA1b_4R9G6_sS6T|pnx$cR#{nDA#HxVU_62W`2czkxd?4&N2`y6N zxdFw0J39(OuZ`f%*@ccw%>pO@LCYQ>!33OC;fQHZS3_c4fRKs=9)p?p&*8^HLpCqI z8tOeHPMPbI&LIleaAnJeijH$>Pp{lz_y2wQGtoX?D<|tdDz1R5DiO>TpjY-m;hvrB%!Zf(+)8cB_=VmJ z6sl2G8KvYu0z%B&mKXQ zT$?)`=oH6Q<(ce}`rfKxQAwCSKQBI4lfPOJ&T$W_^H$ zxA@OIB*z@f;{X0yHgF(I>!octElcGpA(&wI)a_vBVxX`_Pc;oxMSAvMZ1gkyvBzD= z-JDnf1&Y4<`jq>={pTkQ4paW%p8PshL#B0msb>2KCgerRh4dHY!8<|hXRkj7C*qx& z5sXOqe?)u)sl1;*f5!U@@}S3R!@D!VyPq!~^#PN^sM5uhH1-s2 zLItGLMnw|_Q@3w`C9B>R#)ei8JrCP=cq51A-6U?Uwp5Zn0gB%M_6ok}S+3?9e+LrNGRepB#&4 zUUY})rlu=ETAhM7e{so_O!Sqc!)VeMsU=iGsy~V!V}#;&Nk4|3gJZTTA65M?u>y8T z#*R`2eC@h4(OwCLOL8U^X4JJwXx95Jz=Lneas*U!-`*ZyNf6{daiWg92w(IJbSjkO zsYiPea|CX^^e0MW4@U7oxLDZ9;W_Ns=R?!&>GyxPCKHhQ69F>ol_INQU~}V5f!K2| zN*FQnr$37D>}Sh!8L4}lsgpdiy_79y3R6s5MNFMjy+t~ZNMW89Fm?7aaC?2+N(ic_ zq$s1}LHGnlo_!MTBjo^gNG6Z2|EQ1_12fDh&qx@V=^!h&&Jpmf5fm8eQ>ShTz^47H$Fx;MbFHR32H**GcXgIY9C(p}x+x*zt^-}yTa#RYLzaPSv3TeB zHE2ec0_lTywpN3LOPE#ue16&pWKah0s#3PlnXR+>3-38ZhH239m;z3L7%Tz-_Mmi) z1g=_=s)9)pB)OgO9bgWaDYdV{x&cOJ2b zCMEMClNN?K7w?c^?#NmjlxW$-nT-(uVz>5sDw?go>Y>p}l3j$E?MCMUPeh_j%EBDKut(Ur6ro+JDzA9E;fA2G*_R; zdNlaQdkU-582L-OvMWD7(k5f30E8DYt<5*m34?NmyM23eZ6QdXjoJ&6Y>BIKN(+3s zPf~|pVT~12`&Xe@_P@S(d*;K#!z%#lt%NZ0pFfI!EPEGKdWVA6?9bPiTVXGIXeSK& zq32G%+lx`WcTmJJdkHc*AlnmI?*nJ*i}2(wuF@JW6V1nim9EoL79+tsfja!26boR) z2OfR)>>4ISH_90V`*Hv~{lHMSGCWIcKh8YUkxku8hoM%NyjbAljpDSoh|A-^@%wNH zD~;l(PJKZ%nX3@=RKISIUiDH6TIN2;r5~qPoka8xQhcxUhaDiu!?;EZSFUR zkFYWz&Pw9Xt^%9aDU_J7M?enyA+i5ksb`l*Fjz5M%`kjg27Rgp<%H(b6XD*YU<2MT zF0%T4k`;3-|L3cqsJKlo8Na0~R92)fp3Ww~L1Ajq3HR(Uybk>ZQ&kJ4oK)R=DVn@p zzI`>=Ja5iN%)(Pu=6}8?4zithafDV=0dYA9z1+71gRx=l1<+v8HgB(pNv#ym615 zb?rrv8dQ#wW5V|TWJ3u{&V=RgB$p_zwyw%Ru;P`3`&_f~wQCt$>#f0m(864Pz1n6? z6q53pPg$O5Z;amz245jg+V>V$XO~>|VMoBz8bT)vkHkAt&5FGAtVCbEHn!!Xbfeo3C1gETLjx{_6DwWWn`k}=1b??Ja1LO&#p|Pi? znaW6(_U)kDe`J2ji1AyY1Qd0L-qvI}Vy*cFbxO<+Fz1D0CWv>j*m9+Q^n(e$I z8OGMq!r=I2^+v=CUU&p#T)0O@bpaf1mnF@d zB@D&@C(_|neSE}*Py6+Jf*#t_V})DR15Q~_zrn1j2>^n?jKAs8vZbJqlWfPpwI6^z zT)zwFP5zVZ4pX>ToyRK)JeVZ}m$b}JNTg4A2Q$o0pr@>IR|EF?4S`VEcf4l$epI>MsDmKC3K3omO;2JDhN*BFCCCiona@rR zx&a}wO!posHK6+bx7Iy8w5RF-^^HvR6ijPA!RB4Z1*`|q4FENo0i3njfWav4@i>6s z-N+Fh8Vz2Q+qcJIdP}(NGM@(TQiBf|n6Q@^k6EHFl~u$O>?2o@y^w^0@cYgP8)@@T zg8R(pr`$MxQ#rc-76>UQ@du&~ReW}^Qjp+LOD<_PSZc2+r{6-w1>|UD+NogyT2$bn zThP^ofe>w9squ75kPDX8d_smf9u8*$`1p*rCL6XT-i^eD!0a2tX6WFP5}{59W#&_} zwc%dOhYD-8U#}&*y*Af8@TXIt;GoPSL}%F!&-9noOSS&K0JT9LwhgfHkyV(^mGYi@ z4e;$7FyEiG=1Af}6XgIk)-UsJ6z@fA8_YQZC>lh}O7&;Frr`E%UQ3|y25WnzM0c1! z>nG=bK?9BAjH<*7Y5$e4Am`bGfWDIOu6*pm{Ba5J-lbrqD)_UjlP}QIXYby3ocd73Nsqq2BpQKp~IyBxFF0cHfg{@wOBxG(SH@ zI)8k`R0cy`{Qw+iATa>RVtx+DsdMv7Hdo#r*Ji(PGsPZ6RauxcXn7@`2QE+#pvm!_ z?Q>axL_(_XRXtQ>wUP=n$)&xyzG!d#p%2t2&~ilN-`@JYd3O$aK$2D)1qK4rif$JB z7N&{{pf7p9g*MZqpK-|s1grBdeW!_E3HAQ*a=OsqjurlJg|qI}R==}Svq`wk zw6Mr+uh}7&zuYGZ#5-u$i--z8aD! z?He-(eHBX5e5EdbqjNTQDYS`YI*}_|-5!W)puw)4ZBR94;7-NpZsypAJn|cOo;BD2 zqaBmKPJwMVKX?&K)&Tfn24?;@8vt`bfV;CnDjL1{Gky0BBwdm+wAQAMY#n!Sj~3ZA zKxLXt^nJ4pYc%`X)_i`}wLQ|N=4y&jfmz&1bp~VeYUDyh?Xrf*`xaj@9t zZiU3miEJ)4`hO^j5h53m*B!M^HK^~U7nQSXA5yN%I>m7*!Z+zIH~sCVRTzuDdkq3-_|Fp?8&bOj{L05TI0 z%m8X&2I{0M%*f`e!Y(rYWV3~1*>uxjfSz#!{F4$8K0%S{-c&jTqS3B4`ri2VPxQef z+rbH+R6u|lm$>H?Ybe$0Y3l|`12Ze@Ma>k9fx_eGL7yOKNd(9MsFd?Dt8|&<7V!A_VSz3K;&c$sdls%4 z?dG%@{dU!jeTy(&pAX1q#5WpTIutobRe*~0hkXz1u~I(tD||m_vVqMD4-RqX%ZKi< zs_2cen{{tLWXyBete6^#w(y!GBj71PG@oUCC;xp418w9Bcs6WLfH6DLlRl_Ilq5JE zw1AQttcl37Q(9EbRL>#di`T~(;Dczbrf_hI5H&6{eI-eTITv0?VsD@p4F=a|?+P-s z7#9#q@UK4U?;)8l{dji9PPGMwo)DpNXNHLnhUb20Ey_c+-mR-O`@!l0sa50o7aA53 z7tn=EA$CYs@gRPLx-%l;T>?`On>Rq6AF(9%6eRF5yy=*}kQa9}`GUuLcUl8+E|jSA zv_c9aZ*OO#G6&GY9?hhc7+}X>rt8ahz1_zE71~r{yQrtO1##X}WGyEM{S;kJf+-U_ z(1sVcgok+dz~O|$oO)qDT;th1arc~4hY93d0U*Nj_FouLuOK?uW$uC8yVnOyWczqz z)EV*8E(`hT>#>~6sp$7HZv+4shTjB-ivN@@Xer0PwFZ_nq59WIgTT$ z_*?%AC}?MR5?Q)Nt*QYcPCHj0B0CpG6?t`%T!8Q`u-@E#)Xo4Ho=r&UW`{D1?g6=D zpa7R20EX*MNwNE4aIrM#X-qgkW0H_}dzuRH!E4CjM|4f}Qo!QaJ~bm0>!(v&Xi>S$ zp4~0DIU603DZu=zK;>R*1sGR-4-Hn~Cm`k!d$SJ6DPa^==$btam}G^kQ|wyYu|4p5 zKNRe8QK#Hk{r(U{ zglNs|G}Jycpa;$G<9#$30und;ebU-7R7l>xU_M5`2NM7bIU>2ybFyQ7A9SrR>yuKE zC8yt@h&gTn#YQl6Pyr~Q16+(-ZfA_loVcs38IA5W+#W(D<~;$Tpsv~krkS{|AXlG- zrMJM`0UYOiI6-)~ICwWE;nP7&6Hi-jCt#=Nh=sa9* z!!OB8gxzqdfHEZe=6$&A|GZFL+OHfo1y*ogTiy6HVm|}4a6|GT2aHt6UC1fj3;SK7 zl+soW_p_WqORxv|4vn>;_(fxg-;?FsVchl~5~VjnYYII5_&pKXKtTP&o}|@BGA!a>fy}CoC7N0$;jpeTaHbX5ye6=7{5X6eaJ9|R)!SD zme&`{qO%R*@*uFkPq&nIA7!v=$v4jnvvjauD;dBh-b;GVxuE-vd^$-tS$9*f7@#0( zRZ=%cLn4oyd9P+rj?V=172S&5!K}l5tKCa{yPwNUn@cLpuz_kEv`-OS#!Ye9&>S$V zTBQEgT!az>kw6w+YNDm4b48$cmJ6EAf=bhyEa!8X$anyO6lqbrkD{!Fj*M=!fv@sY z%2GdD+m%Dovly;NZV1Sr?4qV({9=2C=kS|YXJbvEIa_{1;0l>SP`QAXlBAV0eGt_m zvzz%R#^3^C0hDQGxu8wss&I~rx55mdFv4Q?pv9E+0|l%?qp4JPm^oMk^gjU5{uP`| z2bZ}$4v_h6CCLT50Zm)UYyvH1^a88@|-9=I**;_h7;JH91TQV%C8iaF&_i-U?43m&F3lV1z`YcN}j~AyqShv@FIat zFAP?G5RV&l()wFL;L*jgpzK{UrQ?!adK!Di?vn{L;d&A{_f8-aBy-3H^tm(sUgAU_ zrmK=F#O$}ZR+0!RChz4}*FY!;z&75mnXBQ^YSMgrkOewNW9vRfUbu^S1J+pyEXtoM z$r7s8e+Q)c{3f;sT#ZpnZ|sl(*xMk9SHK<8KKSW>OWsrhpK2-aCII+VJ>y}KH*>Yx zE5mPZ-)Esled$t~E_1}@a#3&vbe9G|!wyhcR_wz;Bq>E02xJ!N_N%7H(R!`9Prnhn z(ZwG;i#0bvKn1*`p!ZPFK?OJj2c%3gHRM4v_)KtlOwajXQ?qBX}aQ2%5mG3XJ& z%0+Zkh4~yeI1r3t+w0A^CH)H1Nle{u=zTA5XB!0Vyu=9u~h{ z&>ky_TYDb|f(IZNzTKah&zoGnqVEA<1C1R-zi}kH1taHmBpl%VTK`p%e`)qa5q7$5 zn^~BvE0V*^C7+@RmS6VZ0d;~T_Dv#y9LRz9pw0tYmoVrkwre_w8Uf#7jZRJ;h8~pd z)Lv3UA4l_<*!Zq#aT0b`l2u*zhxvi8&nwzfwVU-{tHjdK_FZ ze_2nMNVSJAcmU?n>bLMS+&ZloZXOYF&h8dy&=cx=5N&Rd1?l&0<9(sWPiv>a>nUWI z&W|Q}XnY_OU0^f|6GdvY)7Um#-2Z4VK+?g$mDM?g)Uc{&swyhJ`tbD)K)fF- znjSG&_J{L=>y+%8FU2ywhp%k)=)VWhZgmX(NYOA98yBduJ;gRknlUFIA}x4hl}Ka} zp5Q&RoB7unzr2r)3b|pd31d0+iv=o8=r$|JMH|u;r+)3eRt;!opF!HNL8m=a&Uoo$bUwz zXyn!1JnAf$fc}l`fm;nolOR6-A8-oF(I?v72;zq$Y&+6$c3XzxB6Zj&qszNV&VVKfD*jVV^EM1zKeV==ptckyIGw z^5Q@w5`?Qy2acS6SG%yg*IDGMR}LP%Fv{UQ`@GZD23;r(yp4v;x8S=&An&yx5T62I z>O;B|+|r0Up+ZBfSp`)f{@~PQkfVUFO6In4zD3;`5$fP52(VI7{APy^&5fO-yL)pO z_Ga<=6?;-&i5;56lB0aX-hco#D4ff`QYCrei%j4-uU0-gB@gvl2hWmzmpc@~tDlFv z6EL1F9se(OPC@L1#Oxa`ErGU&rcJDk6J-3ooZHjFkx02(>(~k_0ygP1z?~g<%WSub z$+70l)w+ocgZ;P#qV^1Smw%mu_X>rM-3Jw5>xS7kbr_Ftdt+2^1FrEe42$gUP32^3 zxjO-8lyT`0LBbeZVCx3~Fpj28jrs~T8!SeC^iL!l0m)GV{D^?|1vtbRs3CRoD9=Y~ za&q|1-`>isa3_o)E61rLqXhnx)Z744!NP7mp{8N{qWI!^GIqwmxP9sX>!CwGs@xpo zBjUK!)YNWIQ=&qhl47paijW(0esis52XoNv(bX}6?Uxrc=m)OKrwWA$ylgws04Dz$ zyBG*hNIt}KxWI@v67@%3qxIam*Rs4mGchYk8-`e za%LB>jPTOfAD;meAKhAZ9;zZ;nWQXt6G9vg^+5~;w&%*zo?G&>H`}|*G(=F| zOIi8+MU9P`A~aD13TX*sohd{`V0OexZE+{X?$V)Uhe^X!{&*6gK6hYSCCEBW(5`Z} z0DtKpdimVG`VRc#d>D(tb*fmdfqvYFMwgL|{VyH(;ULDqG(`L!RXxB)Uy-h*bZ`Fx zd&9XTkVicZq^kOx_W~GJbvVw`SqL{$CGLR67R+%?WB^85(Y=yA9%! zD|99V`v0qty6K4`HN%EdmgU*n1X|FFDv(^kDa&*BYGLLh5Ap!M38V+L89?d9=u!+^Cj1h_PwR9)sh zv8T~&FE}{Uf4>3CFGiCZ#WsyIz-s@kUU3A7b3WJ+yJID>{7;k5b;0bp3$?zB!P|9!ioT$WFvF_=4*H>%1)f_) zLi28{*)oQg9?Qx&Uc9N}o`d|3fU_+-XnVs1EhpeODCL}TA~=^a&oEhHQV;El7!TAL zzubB8C(eIq0%^xVnyR4pA`9PZ{5wao_iiP=nNG_Aw-8-nbCH>Z0FL(${Q4huJhTL; zu(k~Fu^AWbdG^Ch*(!TOtd?VvDThyF{%*aiM&EF=F-6L}(fww73kI@`@EBVtqPS^o zIXHXx>p-oJEp4vf=F&m;T$uQE-!&N+dh}S7{YfB0J^giVwckwN8LrDPE%Ja^*17Kk zC@8o09722g7;sD&!mq$+OUd?9ng9vhyxf(k$zl$eu~p*V#v6ECVUd~0Iz9a4jllyL z*ji!N2Z!>%qOJ<3rU;V~E9R%cvnT#-0qRx-VxNC+qB%5R(BCL)Mt^{X9i;gtW?!PR z%WzEv^5S8LuHj!>Ku-{Rb-CxM*6@SWg;*phJ^c#&XJg_~l*?|xuHL=I#>A%CPC-9~ zoA!5ri#uLG8UEqNGj|kC>GewIp=SXcOX$wgYwXCn>|qmtOVz_lu&O1nnOag3`Cg$l#;99?o{9Fje_U3@4>@y48m0T)<7RZ?Esiez4oKW z^nlzIyF5GC3&!gWkPnu2EMfEsHOYvA-9VNEEOx@os}5O1U|E2h@f~$?bT1QH=>H+B zCgb1`K+Z}d(Sk=OX$X}FfD$(AXV5y1D5MHKfJFR=M!VoEnU*+2{2H}j7zrsdyB8*Q zQUA1Ka)c@t58t+cBuT=n0q{H!fKX9U`3Dz#3ix9w4qbTyLHZ+N%g|H=G{OR4#e_>{ zn-D^vMn>leY1u`a9 zHbdoD)-cMKPN{l~5 zPQ!-WXuTxP$U|vwA98S})9M<> zRCZ%jg}4e82_&i(5C;{Z0xyY^pW_Irb0^5g^KC71!W>Iw{sfD!n>GcetyeepNbGYm zz@e3oAMdZy0ej~YGaK8~L8%_)myJT=>X>u31*eUF7Bc1k(=o&CShok4!L_31@0gIh;xbm;i2h zUmz>c*KWlnCSLwO4|w;V5Df##XK4=}tOTey2uk@7wfZUM{Y#`k3o5RS>YPvxa zCM_*O?PLT2!g_DePcYBUdrs)CPWwZS6o9x{3H*DPyECEX)O||HXB@8fXw=u&hfzq` zvc5hOZ^0LZVco(u;KQWtu6h12i-<)rl#W5cqPm~o-*rZOOjC&%O8s2p@$VrG@Q~kQ zV|~!j(U=l5C+D1O1syqVl%fXn{a-Ym z@;1THtH-lnKu_N`m$>a~`TY4N6$wD2_1^8o@3-5JH+^}9voP!dAY%{m`w@GVk9ram?5S0wUeWodP+MQ<^KGK8aa zKf^CbA^Ai{^ZA{nzC|rvj=>I)GQqNoC4Z@%FXdQV4MVWrP0keGAhaoj}vr1 z8n7R&nH|;~>PFES+C&KW8!7HK)b}M`)V)<^^)(tsO&ZI^Z;wtjbbla z0N?yC^Y^y4wiYXXt8=a}MfmIg`e08%7|m-OiU=zV0#&R4zUnODUlxz<6R;k5lvczF z*Mg?Lf9muV*;r0Ae~+qz&m#rXeH~;0k`LU0#`HiV%Y)%zS-puFG zrVNf}rlQvh);(EyWozTRunme<>5nP-}eJj42H{oDP}J zYuJt7@__qoeK#A5&#`)~iD%7R1R8X07LEJcU%#$@Z1)2-YIt0LgUAgr zFmrLW{`X;!8swAA5ooL;M=yOym|6TrS1~ltLGTHynb2eRNV(7FYG`Vff$(So8sm^nlZS^#<+Wyp)jX-HJE&H?>+Fn=1goS3a;sL9 zeR=qqqCQ5srOM?bzUJa3A3MwjdC`z#9u5<5Tv(PjA12hqw9`+Tf z;h9-5_4R89H4t|%8?utzNl*iBWe$B~s%cQfzeC@uB?HDB9B%gNT3j(|t=8L%Ea(cD zRI5E|+@K-t?&FW#)BJ)B#l-%yrljC)-zpiEs=JY(%E!dS@E=4O;-fA~2iK-O%|jX+ z8;4s|6czV`lfjec4PmQ8KqxkIb1OuhEKo9+;#dZ5FIobd|6fI+8W7Un3T-HRkLx*f&KElhPcI@~6!`OF# zbJ@24Yd`Iwgh~=3BuWwu6;gzhtSBNf%8EiI4YJA%iAuC2J0lua5=GgfL@7ihQT#vW zP3sxI_kSEc$ML?;)Azow`?}8gIX~xlHL5Yk-tL=eT>}sSQAUx4+OyzAL^PL{{0L*q zyx}41E>(@;B_$=)4%2p~AtHkN26$wYutM){MnoKCH0fv%oJ?bKe-UP*ArNd#9tpyB zoyF9m!oo=ATQ5M>rtRy=&JzB%DvnSwvB(D0Y5! z$M^{+rPz)aP3ki5Dq|E0VhV*pahM8mSffL&Uk%;U0WQ|+Ie*?JZToHtv-d}N;4fA= z!ok&69z?1}O%RokSiuR*emsb{$-dH|{a)<^in1J=uLRX(8q`jr35%OHZoI^-RW;k2 zYvo?(myOObyTcbor>-cL`-&o6=E*wxd2@jVer;L10%Cq4Kve%FjaLIcX6xuRjI>W~ zla4EmCBPopa=@?!r#r3v>fF;l_=W8^*!^eBzpDh?JC{gK_B|JhtT+&bRU0DYHyTu6 zIi(t;nH)QoDj7Sisp70aCwvltg6*>z2|&Lj(#^ghj?@9cE36`H_c+9tgNi%opjU!Q?_Bga4%;+>u95# zHIhe~jcszj$n3+ll?o~5A?NF@1_ljgjiv!Nsi}=>YJ1Bs*FAjc%he(vBLSd~bPg78jQ# z!0aUC4dV3_-?q<%RF3ZDwFYc~I7l+ZUQ=?*O^`mUZERYR#SOhbxadV`*-i@%Z+CaA z>aEaYLv#!5e7uD{rg@NCnj84xBxIBZzQ16fDrB){3J-^g^(Mb{=p z9(Pr3!AfEx%paEZ@Ko1$g9tO7QxiB0sD6xzFWQhT;d%31;DvFVV-NMTUu=b8ubmRL zNx*j9xuSCPw@=SutT%nTD?`% zVI9mdXC0T-np%3?9=`;hvgwBE#bebMKDDKP)V8)3XP$m^TA;r_)4v6CpY~XQI9Q+( zMKdx=>*k4E`7q7h09Z{Kl<3RaXNVE{(2^-4ArZjX+BIXP9lLKTgDQP@gGuN{fF?B} zx8Ph~dooJ0`eDS)znWDWpv2U%(Km9-#TVWF06KJxjrj*vdRo+kBSRU0WXp?~80tf7 zX)zZP5Qtz5VE;r~hJG!St1T*hMIN7wObx7z87dWth&NQZ8HwI?$f_daU;>qbE!5m0 zMW7(3wLVN+iQuo7^ROp&qTtb^IPBUTodwWmVU((oCp1}(C!YL|mAJ%Ck^=Ge?&y_3(JnKEms$r)+Kk7z2o{M+Z;h6gFvJN(s%A|@mz)d*}`5M0i_K8CFJmHLh= z(}67pK(n+^H-_c3w0svD7%0zpoo};78_5aq@#Rn%6?|u_tPJ9!Bc3dGKjH)s?KY;_2~*-pMJ zov$TeyIve5f6K35K9v$#5o?4jfo6``e>h%b6O0K%(siQ--%7DNsPt_&S6Zl>4hF&1 zVV{|k@qsZIp7wQ<v3*@!NI1WuN-)L=biEG!{2)=q0qwf=erK-gCG)u6sk#w?#pbp{Og8J z$}Q?#MH%z89?goj#%6beJN+Z=6S0o}L^5kd29^v2k_H8u) zK+2EU&{l;aNE|YqJDs}m2?>H=6l9J*h2wqd@etW4;je77XPZ-qedzOE$($E4yO=8^^^>IT-|>Ci+05Pg66DV@qYw%b6`w4IzXUfk3wrJgEi2>$ceY3dMy!MOl%Uk)xp<&{UZ8rj?+a1uX*~W+JHq?8mLA1V`~!L>N|fZWM`lCR^(M}ByI%?}#=1QkPbR7h>BHAwn~89he)X#qz{IXaCO zN5!cEYZai7lsUhOggrhhztq^Qp6wvB>%mBA=ia45pUp2NRf!n^`w&bfB4W00@4(3o znu=4h!9nB3jWY)XO=NI_VuJJzJt7GwsAV||OZX)nk&m_M3i_`4KU{{MQ->URCFvdq z=yY4tV#@>Q8Qi2_TGw39G1^G4;PK-Gd}8VdAJ=2YYUUlHy7P_o%8nBA?7LHfy%qI6duN%M-GkcT*=e{c^+^}8g#hfTV$OSOsb?sAel%>QYP zN!_>L*A;-W;;Z5?wsM$@{Y+=C5#LwlMHFr#r{U=S^zm`MgEs*K_-~;<44-J?cqLhj9@q7Ps=Gr5q4BWuT(FwcTeoEuj9{ss>`c?xBbIX+ zVB^1+yhH;F1&h)>nq#>4?Aen(;_NV%cD@x|X!Z~2lIW2LTNm|MkWEz2Tue-?O(rPi z<)Ozk>)E~trMLd4<%p?dtz@$Cja3&uVW^~zs_GdAgh6&D`RwkIfmL*h{)vf8brMac zI!`>TEUDAf*qGX|ges4ge>rwOk*pQ{m?i~Vf8?DRE5Fj<(ykC#gR}#op*6+R)d(ZT zzenGM;3SrN(UF6~)oj*o277ZGX>=74arN#VTJ)hHBbh`0&VCmd{%@CJO*MuUFBa(Z zU1bX5`&}3mnAv1x2YO&PtZGJasx6Qg2N@Mn^V3mJ(o zS>OdbWVa_Z5&j&_0Lp6ku^_Bi?YZ^(>$s_1Aj#y}1N<1RKJn<6ISHM|%aLWcUShN}ksde<#&0VELd(aGC!?Kah2}UEM{S(15=dOs4>z3 zo^YEH&!R;|m_)J%7}gbZtAyK9<633Hf}d}PV(EbFRx`By6APK`A2)e&3K#{FF>}zQ zQk@K@p(ys@j9qJ0K<3G#5#|tq3ZuJ#s41cN0zrb1lL}4GSvR2|WBT;zyAj&jkD2R( z%GsRbu&AOdz)u7l%ANT+#tD?rKn4`Q%2I9i{CEJm1qL60j?V9oP;oOL0}C3s4&rn< z2z4X~L#fs0=>!Y9afbwuD;R;c1B+L}AM~u#?+YLJI`{PJdDy((hPeYKfF9$Kw^m^I zm@psTiAyk-C5Xt1jZe_ou)%F5CRw&|z;4a$tvWLB<%s(9$zlSXCDblS zR|+77D}ulqlM$zlOaxHzC3ThaM3;KlT&mB1;S2UIF#)pR2wb`SRA%>)fsX@M1W4b~B>92MCLo4% z+DX4JcA!^u=mTp%9)7#_s?LL^;_!W@rl!mTm$Kh+?n{POyZ^eO0nhu3hNjYtMnYqP z4jSnf-=j7WaL&kDmO3jZjB_|C8=Nxg+vnTT{isk#lfQH6g< z?V^d^{^`@FmK(8|@rVFQ%BM{6Zv`h-3s`Fm&U{fH;@ktp$1WhAaY~KFuFoEPSo9Q( zeyYyIWK;m}5wz>ph(aGfd6ER`mo^*{iW+|vbQ4<~>?0Z*5#;=R&&u(KU}@SLGjk&f zZMGIw4_`Gdd~F4c?w4ctLH4^>ZX$5T&(Dz9*%1EH@+pf&r^8ajBZ5sW6zV%Px=VO5 zZUyQ&q;II&B(?CZ#jv?2VlhLAv@XSn4}Op2XrrvG3jr+zn|gS8UBTuER2THaeN6$RtOeu-s?8%` zi(mgSvq|=a%rNpOdO9R_MbVS6%LE@DLO9r&#Gg8DdJ#f#OX_Koima2odtIkFi%6fw`4 z%>c;t9p>yda?_`bxKerOzc&O|&`3~2J0CA^1*RjYFsA}hKhX6~t?%7sA7LJzWB(s} zGS{iyg(yRalr}PZA}U%8FJz89xqp|cyuNFeI_=5#jtHfH*%1yprrECI?Q8ExOkkrvRbp(EL>g)U|g4G4f>HmF;`~92&Y$3f%02bZ3 z7RM~bIgXc)kLVZ}=H-hII(ShvH^9zFud;ke#2yz}#x(u5ukaMzMbaN>0&pwAZe)Nz zb#{s%mZwrV+7EvE^#HPz|2*XZ2>}`sVS#==YisL4+csFC{80=T^2&^fjNP;5Uu@cT zTv0ITMqnq)Z9XJjBPeiQlsQ}3uX%E|lWaPl0Wwx%(b~ceJiJIX zVvAOSbQt3dJ``auVc5TzWqr6^YE7YZ`-eruSe-eK3kwsm z6diMO;U96zk7JcB9*K0IrkvgXpm)JRoqGzeZfw2gOC(deIO0nX=m1WNFwK24tijN- z)LesLkx||M`VO@onz(_ug7GOxftbxec$+4agEd*g?+;qTf;;iIhTOwHbrzlBw<&o? z2>FP7%v<=F(9jS4*4v^t&w)@hVVWSq%^|TGZ3M^g@i)gn#WVD0nPb>V8;d4B;SumA zVd$IlEq%b8|68hNBI1Hx*pImvHRQTej|^lIOaZ+YS+vOe|JL`e^t$gwR4WF!p9I#L zjeVYam&Qp)Daa06 zZgq_IsstXlMp+T2XgHH%Ffub3+AqCvbPwcS5Dm}M7c z4XJGu0VT{EX&x9rl|QZDAFsRy+8zN1bEcZGBb)lX& z#AH4GH8r}`3410J9HFHV74XZw{h`4qOMDYPL$QyjHWvTQqYT3N4wyqhy!iK0m)r5h zYuH)pMStWiL0v)D^TL;(JbAJT8T41%xyaGGn)~4f={G(p>_Q018$@yoR_S;SW9cs` z|8eFBbyv?0*?w{Ds1K#lK7>n)i;IIka4-7ZV$JVH9+{($Leu7*u5`~LaFUgntQ#NIzsEMJDcXokP ziNDPK&%eC>{%n-WrI*GI0RqRyGV3_=V;x1@RHb}qNKo!7J7BhnWGo*%d`KhPlQDYh z?+Y&~GazW&hdvb*+GSR+*PGR*eV#mK?#HSmk5E4Xh9f4ZoeXHq8^gs|1E$st9>8CO z%~3c9NlF9=ssnyLsf6y5Nz9tw8Lj2e2n;YCvaN&@Pa%99_&%nLkq=F&uit6!_7XJ# z>KIsbXArBu(z5U&WN_$6f4=RvVnIA=TvY0U-lXq;nP%rPR0dH$5U}f?TQ(9|f(2?+ z=%rn5e^d|G8##A9Q)r8FhYG84Gq}D{!7cHdgF;9#6s?0BJ9rQDiQ1TH=txchv_upt zNo8|P#G{CmDLwd$8*Tr$Z~U!flT2i~>h;vT3T^$#>51?cOfR_o;h0X15)f!~E^8&YKg2 z$nGg$ASUOx>GYQ|HjkQGLf?Vt`$E|k2#g9-YxsRJzn&er@&Q!U+VQyEhxL%8TDzE* zsiSciM@u?-3RnKv>(C`%nAOk=B6Svkm2ZZ|q6B0w<~ph(uNV2CJJ-gJoE`f;?& zQtl8fq(_kIm`j$FV&sVh=nMAhJ6c(BwaG;q9E8~ngFMfOer>dNQ;cwIzF<6oEUu?83c-t>wWY`HH`^mkd)DWhcnj(n> zz2h0cC(UY%5I_sbi9snItF95C_2W}@ILJzzoC})Y@vgDE!CWN{#ExgzRk+7YV86HE z3{#ug$hB{t#*f!kt|fxvt7xjTqOP7k7UOr#s2fOwOmN8+59i+I=)jPWjV{co{nv*Y zq+Pc|5x*@&;{;89>i)BYA9ZtK!q1KUaTo^saewOv%o(c|0ySaB7eyL>I#}cReMg9y zc~YNbQB%O@rrVSe+AbY4cJ@DUVq*1x;WPp(oC;f}VW5Hr4p;P`8v3xA&7Qf6(_Krdm;&LUkCNJl~hI9%${ z-ZYKlZ^VrM`mvDEV}P5xX@(T?S)Hw0{hyqdD*b~oa?~KoeBtGS>*6;Cm2)Cl7NSFl zJx#hv!wSKn)`aoFQY-8FyCtb1>DQ@?sV@sq`z1BM_Q<5J9pD~?CTz22nGwo5RJj!S zS^oXc-^zgJMO{^^Trh;zg_v680sBw_003k2KQ^o$vp}dZkp_GcBJ0dnnP{p`NjcEK z(}S}5pKnHEdG;Z+To5p>4;zt)v_zeqv9-npQR2PJVey)B% zN_{fv={`7BPusrZmRH`DMi);`*+NXRlG4)D0LHDJc8R~Lv@q0XpXoN^fE`9y6{HJ< z4+C3tmy<4f&5!6t`y%}`vGIdkZ3_2oEBc9eW zF}eDC!o7x(>TG{Gqb-$N9gyzBb%8LjneFfXbkn zx(Rv|ME;Ua#va8o-}&w(JZbHMvn$M1!Z$3#MJO~ai~+yY=+A z7+1(5D(F}c@#_=mfFJtp1Y^^7mK+ii8n{3W=JV#wW9HnaABahR&+ygj=NPGQZ2gxH zJ!*M5AFwwLB0Y2=jhZIvJ=F%(~*zO%4Jz?R`(-0;LBZIyIzBf=94Eo@5#3;-i z`JhplPzikdT}J3KF4N`=i4HOr{05GQZ$qDlU4WUn`AxKZSc`QTHX>s!bdZ9Xbvr!AqTk@?f(7}|FJ>2pJ5~0HkN~Cph*R1 z&`GGGAdSm!$}=bkxTkKc`uj(U|3!*u3jaO|&BKW_HXQ8N+WSr+)4@Zm-Z2d2U{KP< z3(mzy6%I)peW2?CNcgem&$p)JVWeUaxugeKxcM#J>8p6kafaQ^s+#OCW~3afJ}BZ0 z4MYXUI7&-Piv~_pbVR5;Mvj=HAusUUx%@%udHYCz5hJBvt0V!q&k9YHJ$yJ5<<)^| zkzItP4bce(Bg47~b3wy`DxZC$NQX&z+o{*29XxN~5V^$5prO!jFE|z{d#eMpVZzvN zqm4FksF(RmK_%X3!2dc=e2J4AXRDrr(*g$T++83Pd#8Azp`l^z8w7|CXCI~@V_4SO z;4Qy>-dUadbf!e{7c6-)1A-Ed>{N@IPN4o2Hhn?7jm+jS+5>5!A>z?3RzfJ}4mM=S zQHu!@;ya3Qw+?&x_@of&w^g}mu;rjf%1H6|*D+rQ+1}!h5)&X*>I2nraJWM=pJ>u3 zjcK9oLdI3yQxVuy;2(d*Q*cm9nbVWR>G8}dh#t{LMC6poT9P_lsDfcEjPY-MF9p88 z7AxpVhOK@g8aFmbZpTF`k7+^=I%<*-Q&9J-GB{7TV|g%&tY6^IXSA_$OD-d+4MRH% zqVQ>3n-j;v&z#vwY+R^53QC?dlF#|jqgJ#n_HwolbY7Vt_}hvVGMSzAkk#VY|Nglk zO|GQT@5fwSV*nVDAo1rjKNR)J(%c&8FF16fv`GTvCKMDL1s&4i@C)&mfBRBQ7C?{LD70zaYgqRUHA%B0UmxoW z3kw%wL=4R$JAkS>W2ffT3rZK9iH}qg)G1&OTF-pwM!fP&WF#+5Dj|T$`A}t=omn5M zbcFDNfIG;bA357dE?Dh=|GXiA`t@6KR>%eDE;7QZ!M0q6yG&_@BKo5S*>-;|FE}lJ z`PcW7Krnr6^XiTa+@*#gj1j7z^r`f15QU4tD71n5GwL~IzyAy)`AW5uLt;VXsEY!y zI_uhA-Zi7l!XRfH5fMj?8kOq$9X0TwzPI7N@s|n(etj;pNz{m!53XVhsw~9iw?Csl zWbBC9ji}{~>S|KuVGSKuru@g6@1J^0qn)hZY%s&svDLBP5WZAF{%dB$$uLf6xJ&#+ zPXVC<&%slgz7C8o=ZQHkkVD&!*K(MYnMt0V{3L?JWKv!gT#AvQ$b>CDD~;B1sA>3f z49OO=(UWjU+;i&D1-OcOA#NgA(x6HW+U6|~Q~c!hWks6{%>S|OX{Y9lAfZ}BKX&#G zzHq@(->Kt7-}EI*mp;ev>*B!%!Qr_L54{6^ZZaG;y6r}wX>fyMkX>~S@FN;_rhyCn zJiyllqoxv0doXGH^L2YL&u{2;w?R3fNrf>W*R;u&xE#?x@;!+ncQZqZKYRF$WP??g z`A;2^DdrnDW0{Mck74lK7D>CZ=wL$n5dT-8YY39)!4Ib87k_;tBS`0Ak~+q0 z4BvAY7zK($t&_eH(+>T($H$B#kE6eZ&428VT|MQpkdmp_=u(=Hjw%Fd3QsU(ZXYqm zG1OcW1#a^<`Da16UO#vqbN*wkcTjzxIF}}+fOuUyBc7rja3v_IJ$Rest!GrsUGWHE z0oH<(;+Jj;EGYo(7OE;a+GtfhvWaE54c1;r9=4v)@>K)hY%t*?1KHLfIMaSm+tFx^ zmMXvhM5FauYQ~J{^MboHjKm(T0F+n|2MB?;1w0H{w8uq7QB2tEbfHX-L-p5pGg~}% zLV***umJSbrs0WTT??>s5^ks&nmu>%fBcqO16>m_P2KTpV~_|YexZ<76T?9T-+|D6 zs16MMje}3CghmXV(;MnWT&D<<$-2qa)B{Sq-@pm2`z*m0Q5Fk-$ARRW7^%0{p6Gkzn zRq_gx_{MMk^T!l3tTWxI+T;oaHm1?K4RQ__g?VYtQrvY~_aX`> zw|Br_1jbUY*&8{Xr57|3-^iqt-kD5^M?H&Ty+IcQ@hx=lv z4Vy**k)K-S+*^Ug(DV@vP0bA#nZLh0CZJ5|&s{(`(#u&ee6-QwHGLO8b6>#pPwF=7 zR``%m4EJ0G_IT}{aJaH4RpzwLmu)nQN-E{tE0PqYtrHVh7P3T_dG-vfWrMMCl=KEw zNlOe<$+^Bg){>|+RG#=jz*l{psG+?iCag@=?3%=js=Z7*-9=&4TNP;FWw&B626F@A z6cG@}*G@EfHEE^{h|)}G@qhf3>tg^7DZSfWWkwuc{u&x{fDzx-FgCR_k{GvBlekQK z{%@ZzWj2Y~eo$Y1Oy(wXDJkE<*jGzJ`a!}b@Qm7T(DH9UZN}u7*2R@pnRxxNe(RHr zWW|H^Ha86umqSf_&}2z*9N4|xxwH0FplziU|Hx#}=A8~GTW@w*qD0&DN#X(Rbum}U znDn)P2fKeYBH|tbgI1c=10e2>&T^Dx=_(l-1n}jNfGCsGpZ;L9*6dQ!GfvZ(MB^cG zWO8<+sjlLyaRuH8^t+t{6QdA=F!oUw0IDddLguBVrL_Uc%tky~M)y6=yfdq>FJuBVa9)qw8xwM)TYE&z2}TgX z#Dyz-5Fvb&@;qwOq5Dap^=Zy!aC<+zX3C*<4AR2_6!rPH8otn$*xs5nT6=tqdzri$ zye3>BFyNyrd#W}$10I*0ifIB~e1-|>h2*)q3+7xqY;IU|y?HJaRCr+dmD`HrL3DSio^)2)smGw#6yte(?%JX&P zdG5~?6Bxe+)Y8E7=UZ;2S>XCH^w2b)dN}rT@HPHsLhnd@9~NH?ynbzOUyt~xpJ&0G zt_QpSDDEBhj&MQMV1kF9$;-(}H9bhhB{YdyY8SmUqnBr`Pui-y?T^I|XFeY7j4bfY z$DUC08JMy58+IW}sU7JIe}HzQ!MPmYJojD;xt{#<1Q^*fg6y5+Zy-R1;5SqV_uRjK z9|Wc)l>PR7taP17+n%>|-HR;}+bp)x-j^SVm7vD=(fYYKH&fB%RZD0>+|b?9yDnb5 z*!^Iu<`DsKZ!<@4mwuu8`}&KH(eQ)%5BT=QJ1lOD86YZsLJ3XkAgVO@ zYi$Xo)ROt#6>R8U&aHp@eatXM3B*Sm-Ok96v45DSFxPoE)ZI?fNd{MsQjwMJAq-7S zz=fu3^v5e*57--3b?xN!D|@e3UC+Iqv=_m(^Tht6vK%ycE-*CIj2gv(V`+iaSX)pGjRv7s>l*vuugky5z-XiLD~r)L&>wXvA!@VK#Eigo1Wg5ZyID*lZbxB}UwOA7m1593>hlWH?LB-Yxf~A zeIX*i-jD$`k*%zMK8V>z1?=OJv{w!2Zc70Jwi*OvBgk?>d;5NZe&`A$D499+$B;^O zuDgC>@1?3=d%~CELYAg|JDxN5%9SgXaDBCJuL7HHD}9b;m?|{O)eJ;Ek_nHZSh8RC z$blDYl2nzq&Kf$J@B5eyEyjkfJ|uH69JJpb2GOx8cu&n6XP}h_8geI2k{${9{dT;+ z<+{t>iy=ch+tE0OBE2>DA|?zxYxrQpiiSy-Q|J_k8~9!~VCR_nwlLU`rn}DtsNEY9 z{xp1tgz9fw;Vt@zNqD8PncJu{1w(vvfT&Yfcw4Wo^Yz|Ok439#);^K$$I=#z=uNmW z`uA<16v{Qr5Oe5le^3~4HR=USMxmxGKw(w0_GRqCWD6U~<~;P1B#$Fjk^Q=ebhV;3i}n(j*!VE z;oFWFf3Ms&;>B7CHH)qDUu=}XfWE=~Pysuef$|8lS3l^SS#@#U7;=|T#Mu zOPSi6&|G|V^^N|*-@c1k%Lc5)y}9!_H67!AC?ZuM(5YE%+pq8VWlqdCJO0B?#!s|6 z-xemVrn6Bu1PilJ2-p-J53#ALXT#dLao)mttM#HfJ28wTq{f;KyVE)Y@jHJfy+=#8vayb8M z4d;Wia=wY+>#lJpTvl4mDRdfFt*$~F(uuA%dk|SKV-}>T-C4{lT?vEBi5uVIBX|{? zl7#PN+D!QM82S`i+SW6bYEg5&E*#Wg)4~nTp6p^gXy2LgHvGupLxlnM4;Lth`15b| z$F>E2sj&BUF?@Ay`7-abhK=W>4iv0mK0+KH;fH>_`O0VV_wvl#VXHP>R8K}Z0*w@P z=P+Wg1(+fWA6DErwL8GsxK3*HuVV?sgZZ%n)}sn~xNmLtzPq0_YOEiN2&$soyDDUv z1t%ohbMoqMi&1zpk|n`7c+}Y_yz;lD*j*n<2huxUy1@3qVzt*xie*^Kci8Xn$E|nD zkrhxX_9ezj=v5O3C%t9wd@Q<3@IhvrPm54r;jc~cJ*A~OMHHQ}rRx@*LN@pt|%DO?uI$EjQ{;1PT_{W zyn-{&mD^sY4fcL{nCoB|#`_)Go`DvXj_`r6;cDRAIlMWmV1RiKrZc9!74m~bY!>cz zao!bPA=!QQ$3|O8>{Z;dXmPBdXazk4?h1;hlU-8dY3V; zahua=nzVbApH{_f9_qYPzhXhRm-BA@%01m-hV`0GE9HFsTMNw!gs@4GyA<^To19yd z$}b_oS3`iZ9Q{?L(=u;vh(~@iy@wZ%`EL7<$DCn4&VPH0K&j%xzgUF)(55PU!RgbZ zJ53>Gm*C~C;LsFM2rm9Ulc7Bw-2;N7c&c+t$y;wMi7K%0bKJ&)F+RFYCr_&iPp4Skm+ZE|LBE2cx_b@>M!^9 zBuq@sSys8M?_TC@m6ln30)xkHcSD|*3xjS5Lui`B8ZJx%-G3~raY>KxD!*dmS>_%V@fO{( zzLB~+_0*H0SqEwSLmUPMlZ~)NHm+Qjf1Q71J|f<(iqrh`Ij<`=hB~o@Kl-`3+(Wwx zVUbC}41D$#wkC;~Cj>{t_V&EZW?NLaxEx#JG%?tBHs<*+c+9IfYFTVY`nQQk9`9+_ za^eqvvaEuw+J8`BT3ZCvFBrPlfesjb_Bh~y^~f~6y?AB5zVVC0ZK>43I*Lzm;hBS8 zb&dOastf)0{>u|IdOE`gW`k?zh4^kYSx$6%ZT=Xw#HB%9W#tTHkEdZuBkTNluW`ST zIGp>j{g34odSOo<2XENn}h!M2A|d5Xql4(oPP;-`&a>N%>`kU9pmP70qQLS!~4B} zE3aT(lSKcMFFhPt4?ljA{3a59e@{nnQJvu6!#MFUJ6T(#T^LB`$u8s2sy27o4=%ud zTsgzLaO>46)HjNZBl;dlV&S=f$V8w_nT2NGLO*saIed!tPiK{D@#`gXmJZr`YlIU8 z1)<|!?$~oI59I@Sln)wiCKR1UI3a48-kN-FsVU~#r7WUs+w~e2iSIon`o}t7oe!hU zJ5rMnT<&j%)6{q!SB;`-4qS%;=#5(0yR4+;p>_f^r07N$4(FYf_3&~_ zMwKJf$U(CtCl!-a0u_Bf$mi4%Fc=z9dk=(4m3G_^Q?Pi?<_*@L0rYxYG3Y3&M$jw60APvuAKeFx~3Ex zOzN_Eq;4Q<)3aKP@R^T6{&O)aZ==wa=jbrLmD&`-E`7ipoGB(`a8dNN=7|-n>c2N) z@_H~G8{V!S_!{Re{^I~wOo6Z-sPV8;$-T?*#f0`d_wKAO`)eLssqBG?K#V12XNU^& z#ih?W=GfOvrTFH&RW65Bk<{DSAB5qmik;$>eEmOv_0&y*Ep@)N(n$-jYY*?2UY_H;b$*;FB64 z7b^PSsx$Z%3mP+q4qVDAixE@PkvsTTG@X5kcAm(wXFR40P6L2&8nILkHAn9ZCa%?t^)n< z-3xiZ9mPw5#ZN`YQHR|O#Vr@!2wG1`b;BYH@V^G1*kJzzXZOv&JW_YJLhvUqAg_@- zpSY1TzD)KEVNfm_d}m_9jW=v8`%ON@=q}@9HR~qv%slItulz>9dWMuojgg)o?~LOa z{ES`P*Y5ods7ym#9@i$J6LHh6VDn4%3ZVw&0hmUFLd@k(J-2;^ZSvjBX+0tJCXvZ`iFTN}c+BZ20}mEAlq<&0sz z#GBdHlcn5r*Kg*L3@%6DCL!nuf9vG&Y%;$e@9i(G)sp0w$gJWjBniZxY?LX$hvwmU zOQgT}@_uK3GsSwW)QOt4-t)@O*yOK#!)-lP%DrYc&LOxwvc(8zc^7zeHZYmj0Ea!% zG#mM)S!MP2E)xuU@#I>$V&%rd|9a9{>>8dFAC9g60^-{g%qQ}}P1o5NH-8DZx*Bc* zz6$9$bezV}bd>4ryRuEU`(xccSftFE)}vEhXRlo}FZzs5zStX1>q)7nX0Kl)j`J)u z+tLlAGitQYDCD9mE*$P{PCRdQaqWrMb^Wb%C5G9MV*SGNQcG4E2rHI+kuBo3KeH~M z@6Gg~Ly!uNjXZ}9`zjc#Soy$Pd-{v)5J*B zg`S}sajEu$`FXy)&a^sfp(69jIQw7?vph%{(kgV`aL`LC<^Rl@Wo5ou|ux}i1t*G~QJYy>w zB?My;BoFsE>yL1ns*MJiv?R7W{|xRpH++uKS-@qc2kBZXcD;Wg1iYt`iGjc{&-4>j z9QBu2c!kO&?wMy;^C!Of%X*ZQYmMxrc|m8?KYdaZ`QrsX^~D<=A#yc9Rj|4C8wzlF zS^Xcf{En9&6=9F-X%k&tBn@J}JO*DKWczsDB-^^G*BuNU;6O|04%;OjaP z!oLfn;>U$*q{>)h#9(aacpKHT9Sm0f`QdWOK6gTggfIH^9HSD+*)k4`@A|DaE4xWi zGEF;0-HDUz339s}*pm>hP5t$*lMPT7=Vw(c7~|HMZEGMcc0p66a6z}=(a z!Toc#lfi1Kqq=K0b4#9?4}S~@#(#AsKHBTe+SlCo7r)|r%qxjV@@}y{$bTl}9%e6J z4A}n#bqiv6$AXv%^A!swW}6#Gik<)GWAhs~y_XB&KlBV2+m|2aPj3J`<>udlsa}!xrP5E>tpxk>;nceaTkV!;L}4P zcPJnr6gv3{IQhB}KJ&p-l0pL$hmXvs4Z1c@B-GHQ@t1InV}2o`G5{Qc3yoO1|;a#X>Zd3;T^{4{h5;qIM{hdyS}>>IdmvWk>gTi$tflA?}Mwl{dDK(#Y4IONutwu;^Mp;Isdu)N6A0K|EX2!`!EZx~Ouu7Rl7IZY)c{$;F}-Cz6^5z+h`N8rE!b3MYt7f2oc zOcPIXLC7loYcn?Hbsf;_%aDs_$QB&XfU3ThNc<3n=)c5*DmG2vXJhqqf0AutAR!i7 z(fVGWkpsno+n1GAxVU>X1_C&qn^Je!QTITlk*PNe*AYv=&mkLZ(COC!ua=E)>@`9# zeo@60E^gPdH4KE~0?%z~;Tz5B;r=Mw*kEZ~$TYU)$GH)ZJsUH4Q}mTx`;huWk-)5%Al* zc-nJt6-o`C@!kSJE~b223#Wx%=tGn@Kbg~xC^{EzxMZ(HQ3sFWYA!K<&5cTY$j~9b}@r;tO*q_L-7mUO3X(eegQ0VE3ANlh0V+uSi>O45t_>$^l=XGsIzINx)MExdyZ z{&i^5_JKpnIvM6g{kYmCN;D~w?8uwz6Ka_z$af!E!8H(#CHhlX-Mz9m81RYtRVYs23!L`j{K`|~VFVD+-Nj$|=dYvo|Ayph%T14^w_o2XNbo9_=K)kJ>e*$u?L4?KLzqV^ zLg7`mxX2dH@18os{Y3V9gZW~+I2d1razmmPx;D+SXpT?I6k6two;KdyJzL&@_sD$4#qoxjzzu1g)8$Y!=yGqogej+-2oHRa zSji!+e~s*4#fF1Ya!WM+I{=GqKx@&a`5K$M1Oah!Bk##t|!KqigA|wZD}8F0ZLeR=zOT6Z199c0N&3~B{A&GAn+RX znh^OLyn?Y)T;1fdBMY5GvKJb##d)yH3(t?5TFuDPg&T*1%b}+DvzZSTVD^1CR-t;b zf_#;Ts`4-z&X6D{GFiA1i!*g0*%!-Ryx1f9!l8w1!kT9^o}P`&SUZ7-ZK|J}a<+iM z3^9)ixe4NHqawy~Zp-A2>fIjc9m@ zWa2a^a@m9;Q+9|pvRq)H2Jl0szG{jqwA{q9ISnSoonl`v%)>u5)J^S=@7k@0JQk`z z)c{4Q)9$Mkt8kTwJ0*pfr)r4iDO2C4$jxSlzHO|rDfU8|K$udgVcnwDBF($!=T0$m zlgj2Ym=Y(jM1Q>4X-&C8o&!@Kx*26JT_CY67H5G!jkH-#M-}dXZV=2h4EM+xXj_L& zy@g0W>fkg$hi94;slD~k1SfKwXbs4P5}p^5El~*!HamT8t@*rP?{Pb~-ke8%>J2xo z>_z(PC=)!Wyd@bPxnRM$&Z7$HT6S+ci&v`%eU#~acbW37D24lw&hzqjfz!;whj~|9 zri<`(p*9p5V9(o}$8&PZCO5%sHiHRqC(o^GnKyc>hnr$Hzrpml)92(`=&Se^l$mOV-Oam<82^o%lq%dY8=ky~z59hwdiFlx|IEwe9 zuBdN6o59GqW9MXBxc~ia`*>jc@y9=gEa^4MgD8&*yrqY`3#hy*=G4>PmEQww=ZyTr z9)qv%k$SABf~jF6U0QH!rs5G+v16LDh1>_GtaIZFzO&YIUfC2Ix0Tu422;h{E9e~X z$4H2d!dq$@dt()5Y!`+}OJY3lOf&;|0WOM`Vq1uQsmyc!i70M}?XSPLR84T^uyChO zil`6FTPfeBJATW3uX))l2E)W$D%N;%YfM?v_&QE%UP zqX$<#^CNNflYe~9)n&XZ*xh+@Gk5rBmLm>zc~ zi_%=v4~Yl=cw_d2OogAXY;YZv0c%v9w+zd?hJmvx8~Z(d#jd0IAs>M>s@_cqsZR6A zoyNsyd?gtZaCQf&(ukhfD_wnskLt6pZ0TPc8ujn*G8mJkB0Mk3VadFqeKS@Fe)B{w z&28t}5)|6G5uc>q`Iy;PV)%|cH8?AI!0p1DOid7GrMWraW|q>uYcR|FG_av7 z99eVMC1PS}plNBMMb&bPuw^RM3r0^F?>07j^pG6xzr{ABoHL>M8^vwz?zd{kJV(Km zAw>nN5e?Z>d7lz*kTMQ%9uxvdw-n4}%e3YwcA(sa7gkE++IA00o<<2aPN@>M2wJA3 z6Qx|5Y}$}$S0!T+&b~&Nn}5nIx2f6V-tHYz)WZM?BKPH-cmNyq`iW$n=P9m30+x3_ zmr=q;c!5aJ4&W_UQQ4$|P#Z*_0Y{OlH9y#m!Aqum7Yj`?=38%hSs=4(U1+35iM;8J zM6Iet7Uz>M%x{03WEXhT{eJ;F1Os@<1ptNkM_I5y4 zOSSX<;<_TmEVUft6_Uq?>5d6Xb~$2h8}gY(&kWxTuOQBqQaa*5$L z+$W)Iqma>&J4+0?2*Fq-;?#bF!|p&p#xb{^YN@K835>?~Ql{(#0KUW&?D`17V-^6G1iHMQi)26gSWUX^yJ#37)2N^=A+DXCXPVDpi)uIWuqF zYg}96PIJFZ#WggfUfZxc+qTVYEbm@h8|AHDey#Jla}|q)%QD&O2(PCaCQA~-3JaWm zo-CQhvS%i_ec zb=4OqJ_|HaPmI}D^z8MM<3r#49pWumya>#s!?^!Z40j@v4gA(yp5+Z%iab2{GaFXDPYmi_eUd9-g05*s7q8(HcIC(eIwS3C?j{wT&FXO zybpg#uam=tO_$)%n}?rP%SB^Pv}k`=aACj;Z||(D1_8W_uJ@R4m)eqC=J;N~?sHG5 z>3eHq>-K$R_CqI7|ItJ!k)vvogOobHYySj%9*-5(pO6K9DCriO^d1!MEmof zfTzzaU*rs~w z>Za#{@7e4;)8xZ0x2cV}=J8zdJ-?lQ+QzUeZCg%Vd;Hw={W81rX+>`xM+pDescYnE z&!6Eq`q z@9)bRkR~_ffM&u5Fn>L9l|yu@m_tlG4ExKi?{xO@U!C=Q>icmW?k77~SjL+vu9w|v zcQS3=oJ)(;qOa;a7kkfX=bff7Cvwr21xqe}_?x5$hw3O)FdhpT=L$R66n|06rQ(}> z5ifIVYB70zCargKYwkkY&kfugaLNOG87?1uSkRN$l{Cfb`ie8hls zFO3rpe|&<=#(Mw76vVJgRq{~7Z5*4wXL+RCswSh zy*NoN=&Jg2k@uR$o7vv$8QX@fP-JBCtM2<-l9LerL-Mv9K#H-YNV-43rSPiEXW*h8oam)r z9PcODxuvZSyJV@Bch&5!y`f#Tq+QKC@NKVQ#yGm1qz7Q+YgkNWzvtqoauJ;| zo&z;!IRqA$!M=M2Cw3KJ_Mx2m^EO59U;tg2asJLZwDYYEiJosWuM(wE+yB?zxyLkp zMR8m~w(*#5BCEUx*s3rpD5Ao2bq?t$A{(M04tX>}(`@;t4M}|i zWrgIYoUmLp0>5>v3A;N`n-{5DB}k$3dJo+$4z&bCDtYAk67`FwA;zxmoJJ@ZMdEH; zZv?x_``7$?cDW0R)QbkPm_ZRCh2#u~We0M7YWY17tLnaDju%Q#Ib+3rDeA@8|MW{owvjAcea$IBn z{d$`f*c;)c9$8(7EyAzC`50mX%#m>#%_nkcG`NbL*ye(Gw4yj8;>-?Frsv)a{>p1rqdYBBPUo^j} zrXHk4>?kE|5Jh}k&)y#qgiTUXD@}(1N`$4<*2to5kGM7*e2?~=Px#K} z;J*Kgh2CZ7)BLj#vA3!}VX1e?k?a}M;jsPk*r(axc%v&6305b@7At*5aBF7}>#2el z715j$$NyG6SZc09<0l|X%l$@Se^^e;0ov^G6bhyO4b&Dt_36HkLrTbjbkMSWL8~md zhY^_t=YNDa(LhP8;`yxHpf+OVJpsk0>fve_qfBCM*va9`S8Du`LKGl=0EtCO(UL;~ zNwDZu1vuWG@ut`wT3zJTz2fIq%2#3&9h^4AiWt8eFl6Ww-BMr)E7~^qhQv0H7;8m@ zy7&>Swv*5>ZfCpz-<}&NG3vexc$eT#rpKRGU69W6$Sq!!b_An2gZ4|4*J<`HsmtuN z&e-VG(GrVFT@3pe2FKxKsMV{HzOx~fgUMz@I4&D=Z??;(>|xVJI32eD zY2DPIeEaAST?jCwu%G31T$D`Nb<$;30ezciE4*ko&^<^lix`UOnDRzTwQAiZ%dnVe3BuHhcF{=2?m)0%nR=>%YkpRt23xpI~maWmv zUKGb2q_itPs~d-}IpkhROFnJL`Y-U{;9caZwG1ePqm}IJW?O0iicAu8;;`bEZdpZJ7g`1KJ!Ze#H^jM6*$t`Ea)g42|jyJ zn=x|O_X?1f=;dBKZdHtobe~>p!i|C*A-6 literal 0 HcmV?d00001 diff --git a/Common/Logic/Basic.lean b/Common/Logic/Basic.lean index a385dd8..b8bed5a 100644 --- a/Common/Logic/Basic.lean +++ b/Common/Logic/Basic.lean @@ -9,10 +9,23 @@ Additional theorems and definitions related to basic logic. /-- The de Morgan law that distributes negation across a conjunction. -/ -theorem not_and_de_morgan {a b : Prop} : (¬(a ∧ b)) ↔ (¬ a ∨ ¬ b) := by +theorem not_and_de_morgan : (¬(p ∧ q)) ↔ (¬p ∨ ¬q) := by tauto /-- Renaming of `not_or` to indicate its relationship to de Morgan's laws. -/ -theorem not_or_de_morgan : ¬(p ∨ q) ↔ ¬p ∧ ¬q := not_or \ No newline at end of file +theorem not_or_de_morgan : ¬(p ∨ q) ↔ ¬p ∧ ¬q := not_or + +/-- +Universal quantification across nested set memberships can be commuted in either +order. +-/ +theorem forall_mem_comm {X : Set α} {Y : Set β} (p : α → β → Prop) + : (∀ u ∈ X, (∀ v, v ∈ Y → p u v)) = (∀ v ∈ Y, (∀ u, u ∈ X → p u v)) := by + refine propext ?_ + apply Iff.intro + · intro h v hv u hu + exact h u hu v hv + · intro h u hu v hv + exact h v hv u hu \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index a8e3ffd..509a31a 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -89,6 +89,14 @@ theorem mem_mem_imp_pair_subset {x y : α} · intro hy' rwa [hy'] +/-! ## Powerset -/ + +/-- +Every `Set` is a member of its own powerset. +-/ +theorem self_mem_powerset_self {A : Set α} + : A ∈ 𝒫 A := subset_self A + /-! ## Symmetric Difference -/ /-- @@ -116,8 +124,7 @@ This is the contraposition of `mem_symm_diff_iff_exclusive_mem`. -/ theorem not_mem_symm_diff_inter_or_not_union {A B : Set α} : x ∉ (A ∆ B) ↔ (x ∈ A ∩ B) ∨ (x ∉ A ∪ B) := by - unfold symmDiff - simp + show ¬(x ∈ A ∧ ¬x ∈ B ∨ x ∈ B ∧ ¬x ∈ A) ↔ x ∈ A ∧ x ∈ B ∨ ¬(x ∈ A ∨ x ∈ B) rw [ not_or_de_morgan, not_and_de_morgan, not_and_de_morgan, @@ -125,16 +132,12 @@ theorem not_mem_symm_diff_inter_or_not_union {A B : Set α} not_or_de_morgan ] apply Iff.intro - · intro hx - apply Or.elim hx.left + · intro nx + apply Or.elim nx.left · intro nA - exact Or.elim hx.right - (fun nB => Or.inr ⟨nA, nB⟩) - (fun hA => absurd hA nA) + exact Or.elim nx.right (Or.inr ⟨nA, ·⟩) (absurd · nA) · intro hB - apply Or.elim hx.right - (fun nB => absurd hB nB) - (fun hA => Or.inl ⟨hA, hB⟩) + exact Or.elim nx.right (absurd hB ·) (Or.inl ⟨·, hB⟩) · intro hx apply Or.elim hx · intro hy