diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index d86155e..4d51995 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -112,7 +112,7 @@ There is a set having no members: \end{axiom} \section{\defined{Equivalence Class}}% -\label{sec:equivalence-class} +\label{ref:equivalence-class} The set $[x]_R$ is defined by $$[x]_R = \{t \mid xRt\}.$$ If $R$ is an \nameref{ref:equivalence-relation} and $x \in fld R$, then $[x]_R$ @@ -3409,8 +3409,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \begin{proof} - \lean{Bookshelf/Enderton/Set/Chapter\_3} - {Enderton.Set.Chapter\_3.theorem\_3p} + \lean{Bookshelf/Enderton/Set/Relation}{Set.Relation.modEquiv\_partition} Let $\Pi = \{[x]_R \mid x \in A\}$. We show that (i) there are no empty sets in $\Pi$, (ii) no two different sets @@ -5165,7 +5164,7 @@ Show that $R_\Pi$ is an equivalence relation on $A$. \end{proof} -\subsection{\pending{Exercise 3.38}}% +\subsection{\verified{Exercise 3.38}}% \label{sub:exercise-3.38} \nameref{sub:theorem-3p} shows that $A / R$ is a partition of $A$ whenever $R$ @@ -5175,26 +5174,90 @@ Show that if we start with the equivalence relation $R_\Pi$ of the preceding \begin{proof} - If $\Pi$ is empty, its trivial to see $A / R_\Pi$ is likewise empty. - Thus assume $\Pi$ is not empty. - Let $C \in \Pi$. - By definition of a \nameref{ref:partition}, $C$ is nonempty. - Let $x \in C$. - By definition of a \nameref{ref:partition}, every member of $\Pi$ is disjoint - from every other. - Thus - \begin{align*} - C - & = \{t \mid (\exists B \in \Pi)(x \in B \land t \in B)\} \\ - & = \{t \mid x R_\Pi t\} & \textref{sub:exercise-3.37} \\ - & = [x]_{R_\Pi}. - \end{align*} - Therefore every member of $\Pi$ is of form $[x]_{R_\Pi}$ for some $x \in A$. - In other words, $$A / R_\Pi = \{[x]_{R_\Pi} \mid x \in A\} = \Pi.$$ + \lean{Bookshelf/Enderton/Set/Relation} + {Enderton.Set.Chapter\_3.exercise\_3\_38} + + By definition, + \begin{equation} + \label{sub:exercise-3.38-eq1} + R_\Pi = \{ (x, y) \mid (\exists B \in \Pi)(x \in B \land y \in B) \}. + \end{equation} + We prove that $A / R_\Pi = \Pi$. + By the \nameref{ref:extensionality-axiom}, these two sets are equal when + $$B \in A / R_\Pi \iff B \in \Pi.$$ + We prove both directions of this biconditional. + + \paragraph{($\Rightarrow$)}% + + Suppose $B \in A / R_\Pi$. + By \nameref{sub:exercise-3.37}, $R_\Pi$ is an equivalence class. + Then, by definition of a \nameref{ref:quotient-set}, + $$A / R_\Pi = \{[x]_{R_\Pi} \mid x \in A\},$$ + whose members are the \nameref{ref:equivalence-class}es. + Thus there exists some $x \in A$ such that $B = [x]_{R_\Pi}$. + By definition of a \nameref{ref:partition}, there exists a unique set + $B' \in \Pi$ containing $x$. + Thus it suffices to prove that $B = B'$, for then $B = [x]_{R_\Pi} = B'$ is + a member of $\Pi$ as desired. + We proceed by extensionality again; that is, we show + $$y \in B \iff y \in B'.$$ + + \subparagraph{($\rightarrow$)}% + + Suppose $y \in B$. + Then + \begin{align*} + y + & \in B = [x]_{R_\Pi} \\ + & = \{t \mid \pair{x, t} \in R_\Pi\} \\ + & = \{t \mid (\exists B_1 \in \Pi)(x \in B_1 \land t \in B_1)\}. + & \eqref{sub:exercise-3.38-eq1} + \end{align*} + Thus there exists some $B_1 \in \Pi$ such that $x \in B_1$ and + $y \in B_1$. + By definition of a \nameref{ref:partition}, $B_1 \in \Pi$ is the unique + member of $\Pi$ containing $y$. + Thus $B_1 = B'$ meaning $y \in B'$ as desired. + + \subparagraph{($\leftarrow$)}% + + Suppose $y \in B'$. + By construction, $x \in B'$. + Then there exists a set $B_1$ such that $x \in B_1$ and $y \in B_1$, + namely $B'$. + Therefore + \begin{align*} + y + & \in \{t \mid (\exists B_1 \in \Pi)(x \in B_1 \land t \in B_1)\} \\ + & = \{t \mid \pair{x, t} \in R_\Pi\} \\ + & = [x]_{R_\Pi} = B. + \end{align*} + + \subparagraph{Conclusion}% + + By the \nameref{ref:extensionality-axiom}, it follows $B = B'$. + Since $B' \in P$, it also follows $B \in P$. + + \paragraph{($\Leftarrow$)}% + + Let $B \in \Pi$. + By definition of a \nameref{ref:partition}, $B$ is nonempty. + Let $x \in B$. + By definition of a set, $B = \{t \mid x \in B \land t \in B\}$. + By definition of a \nameref{ref:partition}, every member of $B$ must belong + to only $B$ (i.e. no other sets in the partition). + Thus we can equivalently write + \begin{align*} + B + & = \{t \mid (\exists B_1 \in \Pi)(x \in B_1 \land t \in B_1)\} \\ + & = \{ t \mid \pair{x, t} \in R_\Pi \} \\ + & = [x]_{R_\Pi}. + \end{align*} + Therefore $B \in A / R_{\Pi}$. \end{proof} -\subsection{\pending{Exercise 3.39}}% +\subsection{\sorry{Exercise 3.39}}% \label{sub:exercise-3.39} Assume that we start with an equivalence relation $R$ on $A$ and define $\Pi$ to @@ -5203,22 +5266,7 @@ Show that $R_\Pi$, as defined in Exercise 37, is just $R$. \begin{proof} - If $\Pi$ is empty, it's trivial to show $R_\Pi$ is also empty. - Thus assume $\Pi$ is not empty. - Let $C \in \Pi = A / R$. - By definition of a \nameref{ref:partition}, $C$ is nonempty. - Let $x \in C$. - Thus - \begin{align*} - C - & = [x]_R & \textref{sub:theorem-3p} \\ - & = \{t \mid xRt\} \\ - & = \{t \mid (\exists B \in A / R)(x \in B \land t \in B)\} \\ - & = \{t \mid (\exists B \in \Pi)(x \in B \land t \in B)\} \\ - & = \{t \mid x R_\Pi t\}. - \end{align*} - Thus $\pair{x, y} \in R_\Pi$ if and only if $\pair{x, y} \in R$. - By the \nameref{ref:extensionality-axiom}, $R_\Pi = R$. + TODO \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 9e36bd6..9d05af8 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -1702,58 +1702,6 @@ theorem theorem_3m {R : Set.Relation α} have := hS ht exact hT this ht -/-- #### Theorem 3P - -Assume that `R` is an equivalence relation on `A`. Then the set -`{[x]_R | x ∈ A}` of all equivalence classes is a partition of `P`. --/ -theorem theorem_3p {R : Set.Relation α} {A : Set α} {P : Set (Set α)} - (hR : R.isEquivalence A) (hP : P = {neighborhood R x | x ∈ A}) - : isPartition P A := by - refine ⟨?_, ?_, ?_, ?_⟩ - · -- Every member is a subset of `A`. - intro p hp - rw [hP] at hp - simp only [Set.mem_setOf_eq] at hp - have ⟨x, hx⟩ := hp - rw [← hx.right] - show ∀ t, t ∈ neighborhood R x → t ∈ A - intro t ht - exact hR.b_on (Or.inr (mem_pair_imp_snd_mem_ran ht)) - - · -- Every member is nonempty. - intro p hp - rw [hP] at hp - have ⟨x, hx⟩ := hp - rw [← hx.right] - exact ⟨x, hR.refl x hx.left⟩ - - · -- Every pair of members is disjoint. - intro xR hxR yR hyR h - by_contra nh - have nh' : Set.Nonempty (xR ∩ yR) := by - rw [← Set.nmem_singleton_empty] - exact nh - have ⟨z, hz⟩ := nh' - rw [hP] at hxR hyR - have ⟨x, hx⟩ := hxR - have ⟨y, hy⟩ := hyR - rw [← hx.right, ← hy.right] at hz - unfold neighborhood at hz - simp only [Set.mem_inter_iff, Set.mem_setOf_eq] at hz - have hzy : (z, y) ∈ R := hR.symm hz.right - have hxy : (x, y) ∈ R := hR.trans hz.left hzy - have := (neighborhood_iff_mem hR hx.left hy.left).mpr hxy - rw [hx.right, hy.right] at this - exact absurd this h - - · -- Every element of `A` is in `P`. - intro x hx - have := hR.refl x hx - refine ⟨neighborhood R x, ?_, this⟩ - · rw [hP] - exact ⟨x, hx, rfl⟩ - /-- #### Exercise 3.32 (a) Show that `R` is symmetric **iff** `R⁻¹ ⊆ R`. @@ -1980,26 +1928,27 @@ theorem exercise_3_36 {f : Set.HRelation α β} /-- #### Exercise 3.37 -Assume that `Π` is a partition of a set `A`. Define the relation `R` as follows: +Assume that `Π` is a partition of a set `A`. Define the relation `Rₚ` as +follows: ``` -xRy ↔ (∃ B ∈ Π)(x ∈ B ∧ y ∈ B). +xRₚy ↔ (∃ B ∈ Π)(x ∈ B ∧ y ∈ B). ``` -Show that `R` is an equivalence relation on `A`. (This is a formalized version +Show that `Rₚ` is an equivalence relation on `A`. (This is a formalized version of the discussion at the beginning of this section.) -/ theorem exercise_3_37 {P : Set (Set α)} {A : Set α} - (hP : isPartition P A) (R : Set.Relation α) - (hR : ∀ x y, (x, y) ∈ R ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B) - : isEquivalence R A := by - have hR' : R = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by + (hP : isPartition P A) (Rₚ : Set.Relation α) + (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B) + : isEquivalence Rₚ A := by + have hR : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by ext p have (x, y) := p - exact hR x y - refine ⟨?_, ?_, ?_, ?_⟩ + exact hRₚ x y - · -- `fld R ⊆ A` - show ∀ x, x ∈ fld R → x ∈ A - rw [hR'] + refine ⟨?_, ?_, ?_, ?_⟩ + · -- `fld Rₚ ⊆ A` + show ∀ x, x ∈ fld Rₚ → x ∈ A + rw [hR] intro x hx unfold fld dom ran at hx simp only [ @@ -2018,25 +1967,25 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α} have := hP.p_subset B hB.left exact this hB.right.right - · -- `isReflexive R A` + · -- `isReflexive Rₚ A` intro x hx - rw [hR'] + rw [hR] simp only [Set.mem_setOf_eq, and_self] exact hP.exhaustive x hx - · -- `isSymmetric R` + · -- `isSymmetric Rₚ` intro x y h - rw [hR'] at h + rw [hR] at h simp only [Set.mem_setOf_eq] at h have ⟨B, hB⟩ := h - rw [hR'] + rw [hR] simp only [Set.mem_setOf_eq] conv at hB => right; rw [and_comm] exact ⟨B, hB⟩ - · -- `isTransitive R` + · -- `isTransitive Rₚ` intro x y z hx hy - rw [hR'] at hx hy + rw [hR] at hx hy simp only [Set.mem_setOf_eq] at hx hy have ⟨B₁, hB₁⟩ := hx have ⟨B₂, hB₂⟩ := hy @@ -2050,10 +1999,78 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α} intro h' rw [Set.ext_iff] at h' exact (h' y).mp ⟨hy₁, hy₂⟩ - rw [hR'] + rw [hR] simp only [Set.mem_setOf_eq] exact ⟨B₁, hB₁.left, hB₁.right.left, by rw [hB]; exact hB₂.right.right⟩ +/-- #### Exercise 3.38 + +Theorem 3P shows that `A / R` is a partition of `A` whenever `R` is an +equivalence relation on `A`. Show that if we start with the equivalence relation +`Rₚ` of the preceding exercise, then the partition `A / Rₚ` is just `P`. +-/ +theorem exercise_3_38 {P : Set (Set α)} {A : Set α} + (hP : isPartition P A) (Rₚ : Set.Relation α) + (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B) + : modEquiv (exercise_3_37 hP Rₚ hRₚ) = P := by + have hR : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by + ext p + have (x, y) := p + exact hRₚ x y + + ext B + apply Iff.intro + · intro ⟨x, hx⟩ + have ⟨B', hB'⟩ := partition_mem_mem_eq hP hx.left + simp only at hB' + suffices B = B' by + rw [this] + exact hB'.left.left + + ext y + apply Iff.intro + · intro hy + rw [← hx.right, hR] at hy + have ⟨B₁, hB₁⟩ := hy + have := hB'.right B₁ ⟨hB₁.left, hB₁.right.left⟩ + rw [← this] + exact hB₁.right.right + · intro hy + rw [← hx.right, hR] + exact ⟨B', hB'.left.left, hB'.left.right, hy⟩ + + · intro hB + have ⟨x, hx⟩ := hP.nonempty B hB + have hx' : x ∈ A := hP.p_subset B hB hx + refine ⟨x, hx', Eq.symm ?_⟩ + calc B + _ = {t | x ∈ B ∧ t ∈ B} := by + ext y + apply Iff.intro + · intro hy + exact ⟨hx, hy⟩ + · intro hy + exact hy.right + _ = {t | ∃ B₁ ∈ P, x ∈ B₁ ∧ t ∈ B₁} := by + ext y + apply Iff.intro + · intro hy + exact ⟨B, hB, hy⟩ + · intro hy + have ⟨B₁, hB₁⟩ := hy + have ⟨B', hB'⟩ := partition_mem_mem_eq hP hx' + simp only [Set.mem_setOf_eq] at * + have : B = B₁ := by + have lhs := hB'.right B ⟨hB, hx⟩ + have rhs := hB'.right B₁ ⟨hB₁.left, hB₁.right.left⟩ + rw [lhs, rhs] + rw [this] + exact hB₁.right + _ = {t | (x, t) ∈ Rₚ } := by + rw [hR] + simp only [Set.mem_setOf_eq] + _ = neighborhood Rₚ x := rfl + end Relation end Enderton.Set.Chapter_3 \ No newline at end of file diff --git a/Bookshelf/Enderton/Set/Relation.lean b/Bookshelf/Enderton/Set/Relation.lean index 049ff9f..0c15504 100644 --- a/Bookshelf/Enderton/Set/Relation.lean +++ b/Bookshelf/Enderton/Set/Relation.lean @@ -529,6 +529,14 @@ and the members of the set. It isn't standard in anyway. -/ def neighborhood (R : Relation α) (x : α) := { t | (x, t) ∈ R } +/-- +The neighborhood with some respect to an equivalence relation `R` on set `A` +and member `x` contains `x`. +-/ +theorem neighborhood_self_mem {R : Set.Relation α} {A : Set α} {x : α} + (hR : isEquivalence R A) (hx : x ∈ A) + : x ∈ neighborhood R x := hR.refl x hx + /-- Assume that `R` is an equivalence relation on `A` and that `x` and `y` belong to `A`. Then `[x]_R = [y]_R ↔ xRy`. @@ -560,6 +568,21 @@ structure isPartition (P : Set (Set α)) (A : Set α) : Prop where disjoint : ∀ a ∈ P, ∀ b, b ∈ P → a ≠ b → a ∩ b = ∅ exhaustive : ∀ a ∈ A, ∃ p, p ∈ P ∧ a ∈ p +/-- +Membership of sets within `P` is unique. +-/ +theorem partition_mem_mem_eq {P : Set (Set α)} {A : Set α} + (hP : isPartition P A) (hx : x ∈ A) + : ∃! B, B ∈ P ∧ x ∈ B := by + have ⟨B, hB⟩ := hP.exhaustive x hx + refine ⟨B, hB, ?_⟩ + intro B₁ hB₁ + by_contra nB + have hB_disj := hP.disjoint B hB.left B₁ hB₁.left (Ne.symm nB) + rw [Set.ext_iff] at hB_disj + have := (hB_disj x).mp ⟨hB.right, hB₁.right⟩ + simp at this + /-- The partition `A / R` induced by an equivalence relation `R`. -/