From 49bd4871fe370bf917f7d3668819d716532dbe39 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 6 Jun 2023 20:16:06 -0600 Subject: [PATCH] Enderton. Theorem 3A. --- Bookshelf/Enderton/Set.tex | 93 +++++++++++++++++++++++++++ Bookshelf/Enderton/Set/Chapter_2.lean | 1 - Bookshelf/Enderton/Set/Chapter_3.lean | 10 +++ Common/Set.lean | 2 + Common/Set/Basic.lean | 31 +++++++++ Common/Set/OrderedPair.lean | 93 +++++++++++++++++++++++++++ 6 files changed, 229 insertions(+), 1 deletion(-) create mode 100644 Bookshelf/Enderton/Set/Chapter_3.lean create mode 100644 Common/Set/OrderedPair.lean diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index dc9a457..d8875bc 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -45,6 +45,18 @@ If two sets have exactly the same members, then they are equal: \end{axiom} +\section{\defined{Ordered Pair}}% +\label{ref:ordered-pair} + +For any sets $u$ and $v$, the \textbf{ordered pair} $\left< u, v \right>$ is + the set $\{\{u\}, \{u, v\}\}$. + +\begin{definition} + + \lean*{Common/Set/OrderedPair}{OrderedPair} + +\end{definition} + \section{\defined{Pair Set}}% \label{ref:pair-set} @@ -2211,4 +2223,85 @@ If not, then under what conditions does equality hold? \end{proof} +\chapter{Relations and Functions}% +\label{chap:relations-functions} + +\section{Ordered Pairs}% +\label{sec:ordered-pairs} + +\subsection{\verified{Theorem 3A}}% +\label{sub:theorem-3a} + +\begin{theorem} + + For any sets $x$, $y$, $u$, and $v$, + \begin{equation} + \label{sub:theorem-3a-eq1} + \left< u, v \right> = \left< x, y \right> \iff u = x \land v = y. + \end{equation} + +\end{theorem} + +\begin{proof} + + \lean{Common/Set/OrderedPair}{Set.OrderedPair.ext\_iff} + + Let $x$, $y$, $u$, and $v$ be arbitrary sets. + + \paragraph{($\Leftarrow$)}% + + This follows trivially. + + \paragraph{($\Rightarrow$)}% + + Suppose $\left< u, v \right> = \left< x, y \right>$. + Then, by definition of an \nameref{ref:ordered-pair}, + \begin{equation} + \label{sub:theorem-3a-eq2} + \{\{u\}, \{u, v\}\} = \{\{x\}, \{x, y\}\}. + \end{equation} + By the \nameref{ref:extensionality-axiom}, it follows + $\{u\} \in \{\{x\}, \{x, y\}\}$ and + $\{u, v\} \in \{\{x\}, \{x, y\}\}$. + That is, + $$\{u\} = \{x\} \quad\text{or}\quad \{u\} = \{x, y\}$$ + and + $$\{u, v\} = \{x\} \quad\text{or}\quad \{u, v\} = \{x, y\}.$$ + There are 4 cases to consider: + + \paragraph{Case 1}% + + Suppose $\{u\} = \{x\}$ and $\{u, v\} = \{x\}$. + The former identity implies $u = x$. + The latter identity implies $u = v = x$. + Then \eqref{sub:theorem-3a-eq2} simplifies to + $$\{\{u\}\} = \{\{x\}, \{x, y\}\},$$ meaning $x = y$. + Thus $v = y$ as well. + + \paragraph{Case 2}% + + Suppose $\{u\} = \{x\}$ and $\{u, v\} = \{x, y\}$. + The former identity implies $u = x$. + Substituting into the latter identity yields $\{u, v\} = \{u, y\}$. + This holds if and only if $v = y$. + + \paragraph{Case 3}% + + Suppose $\{u\} = \{x, y\}$ and $\{u, v\} = \{x\}$. + The former identity implies $x = y = u$. + Substituting into the latter yields $\{u, v\} = \{u\}$. + Thus $u = v$ which in turn implies $v = y$. + + \paragraph{Case 4}% + Suppose $\{u\} = \{x, y\}$ and $\{u, v\} = \{x, y\}$. + The former identity implies $x = y = u$. + Substituting into the latter yields $\{u, v\} = \{u\}$. + This implies $v = u$ which in turn implies $v = y$. + + \paragraph{Conclusion}% + + These cases are exhaustive and each implies that $u = x$ and $v = y$. + +\end{proof} + \end{document} diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean index 79edd4a..1cecbcf 100644 --- a/Bookshelf/Enderton/Set/Chapter_2.lean +++ b/Bookshelf/Enderton/Set/Chapter_2.lean @@ -1,6 +1,5 @@ import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Lattice -import Mathlib.Tactic.LibrarySearch import Bookshelf.Enderton.Set.Chapter_1 import Common.Logic.Basic diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean new file mode 100644 index 0000000..1470377 --- /dev/null +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -0,0 +1,10 @@ +import Mathlib.Data.Set.Basic + +/-! # Enderton.Chapter_3 + +Relations and Functions +-/ + +namespace Enderton.Set.Chapter_3 + +end Enderton.Set.Chapter_3 \ No newline at end of file diff --git a/Common/Set.lean b/Common/Set.lean index d031e47..b611e08 100644 --- a/Common/Set.lean +++ b/Common/Set.lean @@ -1,2 +1,4 @@ import Common.Set.Basic +import Common.Set.Interval +import Common.Set.OrderedPair import Common.Set.Partition \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index 509a31a..18c2ce2 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -44,6 +44,37 @@ It returns `1` if the specified input belongs to `S` and `0` otherwise. def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)] : Nat := if x ∈ S then 1 else 0 +/-! ## Equality -/ + +/-- +If `{x, y} = {x}` then `x = y`. +-/ +theorem pair_eq_singleton_mem_imp_eq_self {x y : α} + (h : {x, y} = ({x} : Set α)) : y = x := by + rw [Set.ext_iff] at h + have := h y + simp at this + exact this + +/-- +If `{x, y} = {z}` then `x = y = z`. +-/ +theorem pair_eq_singleton_mem_imp_eq_all {x y z : α} + (h : {x, y} = ({z} : Set α)) : x = z ∧ y = z := by + have h' := h + rw [Set.ext_iff] at h' + have hz := h' z + simp at hz + apply Or.elim hz + · intro hzx + rw [← hzx] at h + have := pair_eq_singleton_mem_imp_eq_self h + exact ⟨hzx.symm, this⟩ + · intro hzy + rw [← hzy, Set.pair_comm] at h + have := pair_eq_singleton_mem_imp_eq_self h + exact ⟨this, hzy.symm⟩ + /-! ## Subsets -/ /-- diff --git a/Common/Set/OrderedPair.lean b/Common/Set/OrderedPair.lean new file mode 100644 index 0000000..aea2c44 --- /dev/null +++ b/Common/Set/OrderedPair.lean @@ -0,0 +1,93 @@ +import Mathlib.Data.Set.Basic + +import Common.Logic.Basic +import Common.Set.Basic + +namespace Set + +/-- +Kazimierz Kuratowski's definition of an ordered pair. +-/ +def OrderedPair (x y : α) : Set (Set α) := {{x}, {x, y}} + +namespace OrderedPair + +theorem ext_iff {x y u v : α} + : (OrderedPair x y = OrderedPair u v) ↔ (x = u ∧ y = v) := by + unfold OrderedPair + apply Iff.intro + · intro h + have h' := h + rw [Set.ext_iff] at h' + have hu := h' {u} + have huv := h' {u, v} + simp only [mem_singleton_iff, mem_insert_iff, true_or, iff_true] at hu + simp only [mem_singleton_iff, mem_insert_iff, or_true, iff_true] at huv + apply Or.elim hu + · apply Or.elim huv + · -- #### Case 1 + -- `{u} = {x}` and `{u, v} = {x}`. + intro huv_x hu_x + rw [singleton_eq_singleton_iff] at hu_x + rw [hu_x] at huv_x + have hx_v := pair_eq_singleton_mem_imp_eq_self huv_x + rw [hu_x, hx_v] at h + simp only [mem_singleton_iff, insert_eq_of_mem] at h + have := pair_eq_singleton_mem_imp_eq_self $ + pair_eq_singleton_mem_imp_eq_self h + rw [← hx_v] at this + exact ⟨hu_x.symm, this⟩ + · -- #### Case 2 + -- `{u} = {x}` and `{u, v} = {x, y}`. + intro huv_xy hu_x + rw [singleton_eq_singleton_iff] at hu_x + rw [hu_x] at huv_xy + by_cases hx_v : x = v + · rw [hx_v] at huv_xy + simp at huv_xy + have := pair_eq_singleton_mem_imp_eq_self huv_xy.symm + exact ⟨hu_x.symm, this⟩ + · rw [Set.ext_iff] at huv_xy + have := huv_xy v + simp at this + apply Or.elim this + · intro hv_x + rw [hu_x, ← hv_x] at h + simp at h + have := pair_eq_singleton_mem_imp_eq_self $ + pair_eq_singleton_mem_imp_eq_self h + exact ⟨hu_x.symm, this⟩ + · intro hv_y + exact ⟨hu_x.symm, hv_y.symm⟩ + · apply Or.elim huv + · -- #### Case 3 + -- `{u} = {x, y}` and `{u, v} = {x}`. + intro huv_x hu_xy + rw [Set.ext_iff] at huv_x + have hu_x := huv_x u + have hv_x := huv_x v + simp only [mem_singleton_iff, mem_insert_iff, true_or, true_iff] at hu_x + simp only [mem_singleton_iff, mem_insert_iff, or_true, true_iff] at hv_x + rw [← hu_x] at hu_xy + have := pair_eq_singleton_mem_imp_eq_self hu_xy.symm + rw [hu_x, ← hv_x] at this + exact ⟨hu_x.symm, this⟩ + · -- #### Case 4 + -- `{u} = {x, y}` and `{u, v} = {x, y}`. + intro huv_xy hu_xy + rw [Set.ext_iff] at hu_xy + have hx_u := hu_xy x + have hy_u := hu_xy y + simp only [mem_singleton_iff, mem_insert_iff, true_or, iff_true] at hx_u + simp only [mem_singleton_iff, mem_insert_iff, or_true, iff_true] at hy_u + rw [hx_u, hy_u] at huv_xy + simp only [mem_singleton_iff, insert_eq_of_mem] at huv_xy + have := pair_eq_singleton_mem_imp_eq_self huv_xy + rw [← this] at hy_u + exact ⟨hx_u, hy_u⟩ + · intro h + rw [h.left, h.right] + +end OrderedPair + +end Set \ No newline at end of file