diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/algebra/magma.tex | 7 | ||||
| -rw-r--r-- | library/algebra/monoid.tex | 5 | ||||
| -rw-r--r-- | library/algebra/quasigroup.tex | 30 | ||||
| -rw-r--r-- | library/algebra/semigroup.tex | 43 | ||||
| -rw-r--r-- | library/everything.tex | 7 | ||||
| -rw-r--r-- | library/order/order.tex | 61 | ||||
| -rw-r--r-- | library/order/quasiorder.tex | 43 | ||||
| -rw-r--r-- | library/order/semilattice.tex | 19 | ||||
| -rw-r--r-- | library/ordinal.tex | 262 | ||||
| -rw-r--r-- | library/relation/closure.tex | 3 | ||||
| -rw-r--r-- | library/relation/equivalence.tex | 94 | ||||
| -rw-r--r-- | library/set.tex | 16 | ||||
| -rw-r--r-- | library/set/cons.tex | 6 | ||||
| -rw-r--r-- | library/set/equinumerosity.tex | 37 | ||||
| -rw-r--r-- | library/status.md | 211 | ||||
| -rw-r--r-- | library/topology/basis.tex | 105 | ||||
| -rw-r--r-- | library/topology/disconnection.tex | 18 | ||||
| -rw-r--r-- | library/topology/preclosure.tex | 14 | ||||
| -rw-r--r-- | library/topology/separation.tex | 23 | ||||
| -rw-r--r-- | library/topology/topological-space.tex | 375 |
20 files changed, 999 insertions, 380 deletions
diff --git a/library/algebra/magma.tex b/library/algebra/magma.tex index d05ce29..3937b56 100644 --- a/library/algebra/magma.tex +++ b/library/algebra/magma.tex @@ -71,10 +71,13 @@ Let $A$ be a unital magma. Then $\mul(\neutral,\neutral) = \neutral$. \end{proposition} +\begin{proof} + Follows by \cref{unitalmagma_type,unitalmagma_left}. +\end{proof} \begin{proposition}\label{unitalmagma_neutral_unique} Let $A$ be a unital magma. - Let $e$ be a set such that $e\in A$ and for all $x\in A$ we have $\mul(x, e) = x = \mul(e, x)$. + Let $e$ be a set such that $e\in \carrier[A]$ and for all $x\in \carrier[A]$ we have $\mul(x, e) = x = \mul(e, x)$. Then $e = \neutral$. \end{proposition} \begin{proof} @@ -97,5 +100,5 @@ \begin{proof} We have $x\cdot e\in \LeftOrb{e}{A}$ by \cref{left_orbit}. Thus $x\cdot e\in\LeftOrb{f}{A}$ by assumption. - Take $y\in\carrier[A]$ such that $x\cdot e = y\cdot f$ by \cref{left_orbit}. + Take $y$ such that $y\in\carrier[A]$ and $x\cdot e = y\cdot f$ by \cref{left_orbit}. \end{proof} diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex index bef3166..ed9d2ff 100644 --- a/library/algebra/monoid.tex +++ b/library/algebra/monoid.tex @@ -4,10 +4,13 @@ \begin{struct}\label{monoid} A monoid $A$ is a unital magma such that \begin{enumerate} - \item\label{monoid_assoc} for all $a, b, c$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. + \item\label{monoid_assoc} for all $a,b,c\in\carrier[A]$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. \end{enumerate} \end{struct} \begin{corollary}\label{monoid_implies_semigroup} Let $A$ be a monoid. Then $A$ is a semigroup. \end{corollary} +\begin{proof} + Follows by \cref{monoid,unitalmagma,semigroup}. +\end{proof} diff --git a/library/algebra/quasigroup.tex b/library/algebra/quasigroup.tex index 747ab03..50d7b0f 100644 --- a/library/algebra/quasigroup.tex +++ b/library/algebra/quasigroup.tex @@ -10,27 +10,37 @@ \end{enumerate} such that \begin{enumerate} - \item for all $a, b\in A$ we have $\ldiv (a,b)\in A$. - \item for all $a, b\in A$ we have $\rdiv (a,b)\in A$. - \item for all $a,b \in A$ we have $b = \mul(a,\ldiv (a,b))$. - \item for all $a,b \in A$ we have $b = \ldiv(a,\mul (a,b))$. - \item for all $a,b \in A$ we have $b = \mul(\rdiv (b,a),a)$. - \item for all $a,b \in A$ we have $b = \rdiv(\mul (b,a),a)$. + \item\label{quasigroup_ldiv_type} for all $a,b\in\carrier[A]$ we have $\ldiv[A](a,b)\in\carrier[A]$. + \item\label{quasigroup_rdiv_type} for all $a,b\in\carrier[A]$ we have $\rdiv[A](a,b)\in\carrier[A]$. + \item\label{quasigroup_mul_ldiv} for all $a,b\in\carrier[A]$ we have $b = \mul[A](a,\ldiv[A](a,b))$. + \item\label{quasigroup_ldiv_mul} for all $a,b\in\carrier[A]$ we have $b = \ldiv[A](a,\mul[A](a,b))$. + \item\label{quasigroup_rdiv_mul} for all $a,b\in\carrier[A]$ we have $b = \mul[A](\rdiv[A](b,a),a)$. + \item\label{quasigroup_mul_rdiv} for all $a,b\in\carrier[A]$ we have $b = \rdiv[A](\mul[A](b,a),a)$. \end{enumerate} \end{struct} % Cancelling an element on the left. \begin{lemma}\label{quasigroup_cancel_left} Let $A$ be a quasigroup. - Let $a,b,c \in A$. - Suppose $\mul(a,b) = \mul(a,c)$. + Let $a,b,c\in\carrier[A]$. + Suppose $\mul[A](a,b) = \mul[A](a,c)$. Then $b = c$. \end{lemma} +\begin{proof} + We have $b=\ldiv[A](a,\mul[A](a,b))$ by \cref{quasigroup_ldiv_mul}. + We have $c=\ldiv[A](a,\mul[A](a,c))$ by \cref{quasigroup_ldiv_mul}. + Follows by assumption. +\end{proof} % Cancelling an element on the right. \begin{lemma}\label{quasigroup_cancel_right} Let $A$ be a quasigroup. - Let $a,b,c \in A$. - Suppose $\mul(a,c) = \mul(b,c)$. + Let $a,b,c\in\carrier[A]$. + Suppose $\mul[A](a,c) = \mul[A](b,c)$. Then $a = b$. \end{lemma} +\begin{proof} + We have $a=\rdiv[A](\mul[A](a,c),c)$ by \cref{quasigroup_mul_rdiv}. + We have $b=\rdiv[A](\mul[A](b,c),c)$ by \cref{quasigroup_mul_rdiv}. + Follows by assumption. +\end{proof} diff --git a/library/algebra/semigroup.tex b/library/algebra/semigroup.tex index e090a56..be94945 100644 --- a/library/algebra/semigroup.tex +++ b/library/algebra/semigroup.tex @@ -5,8 +5,7 @@ \begin{struct}\label{semigroup} A semigroup $A$ is a magma such that \begin{enumerate} - %\item for all $a, b, c\in \carrier[A]$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. - \item\label{semigroup_assoc} for all $a, b, c$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. + \item\label{semigroup_assoc} for all $a, b, c\in \carrier[A]$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. \end{enumerate} \end{struct} @@ -18,8 +17,7 @@ \begin{struct}\label{regularsemigroup} A regular semigroup $A$ is a semigroup such that \begin{enumerate} - %\item for all $a\in \carrier[A]$ there exists $b\in\carrier[A]$ such that $\mul[A](a, \mul[A](b, a)) = a$. - \item\label{regularsemigroup_regular} for all $a$ there exists $b\in\carrier[A]$ such that $\mul[A](a, \mul[A](b, a)) = a$. + \item\label{regularsemigroup_regular} for all $a\in \carrier[A]$ there exists $b\in\carrier[A]$ such that $\mul[A](a, \mul[A](b, a)) = a$. \end{enumerate} \end{struct} @@ -38,12 +36,18 @@ Suppose $A$ is an inverse semigroup. Then $A$ is a semigroup. \end{proposition} +\begin{proof} + Follows by \cref{inversesemigroup,regularsemigroup}. +\end{proof} \begin{proposition}\label{inversesemigroup_is_regularsemigroup} Suppose $A$ is an inverse semigroup. Then $A$ is a regular semigroup. \end{proposition} +\begin{proof} + Follows by \cref{inversesemigroup}. +\end{proof} \begin{proposition}\label{idempotentelems_eq_iff_orbits_eq} Let $A$ be an inverse semigroup. @@ -56,27 +60,12 @@ Then $e = f$. \end{proposition} \begin{proof} - Take $x, y\in\carrier[A]$ such that $e = x\cdot f$ and $f = y\cdot e$ by \cref{idempotents}. - % - \begin{align*} - e - &= x \cdot f - \explanation{by assumption}\\ - &= x\cdot (f\cdot f) - \explanation{by \cref{idempotents}}\\ - &= (x\cdot f)\cdot f - \explanation{by \cref{semigroup_assoc,inversesemigroup_is_semigroup}}\\ - &= e\cdot f - \explanation{by assumption}\\ - &= f\cdot e - \explanation{by \hyperref[inversesemigroup_comm]{commutativity of idempotent elements}}\\ - &= (y\cdot e)\cdot e - \explanation{by assumption}\\ - &= y\cdot (e\cdot e) - \explanation{by \cref{semigroup_assoc,inversesemigroup_is_semigroup}}\\ - &= y \cdot e - \explanation{by \cref{idempotents}}\\ - &= f - \explanation{by assumption} - \end{align*} + Take $x,y$ such that $x,y\in\carrier[A]$ and + $e = x\cdot f$ and $f = y\cdot e$ by \cref{idempotents}. + We have $e=e\cdot f$ by + \cref{idempotents,semigroup_assoc,inversesemigroup_is_semigroup}. + We have $f=f\cdot e$ by + \cref{idempotents,semigroup_assoc,inversesemigroup_is_semigroup}. + We have $e\cdot f=f\cdot e$ by \cref{inversesemigroup_comm}. + Follows by assumption. \end{proof} diff --git a/library/everything.tex b/library/everything.tex index f4eb62a..c7d2e64 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -21,8 +21,10 @@ \import{algebra/magma.tex} \import{algebra/semigroup.tex} \import{algebra/monoid.tex} +\import{algebra/quasigroup.tex} +\import{algebra/loop.tex} \import{order/order.tex} -%\import{order/semilattice.tex} +\import{order/semilattice.tex} \import{topology/topological-space.tex} \import{topology/basis.tex} \import{topology/disconnection.tex} @@ -31,3 +33,6 @@ \begin{proposition}\label{trivial} $\emptyset = \emptyset$. \end{proposition} +\begin{proof} + Follows by \cref{emptyset}. +\end{proof} diff --git a/library/order/order.tex b/library/order/order.tex index 1b7692f..dc9497c 100644 --- a/library/order/order.tex +++ b/library/order/order.tex @@ -45,13 +45,16 @@ \begin{proposition}\label{toorder_reflexive} $\toorder{A}{R}$ is reflexive on $A$. \end{proposition} +\begin{proof} + Follows by \cref{toorder,reflexive_on,id_iff,union_iff}. +\end{proof} \begin{proposition}\label{toorder_intro} Suppose $(a,b)\in R$. Then $(a,b)\in\toorder{A}{R}$. \end{proposition} \begin{proof} - $R\subseteq\toorder{A}{R}$. + Follows by \cref{toorder,union_iff}. \end{proof} \begin{proposition}\label{toorder_elim} @@ -65,14 +68,33 @@ \begin{proposition}\label{toorder_iff} $(a,b)\in\toorder{A}{R}$ iff $(a,b)\in R$ or $a = b\in A$. \end{proposition} +\begin{proof} + Follows by \cref{toorder,id_iff,union_iff}. +\end{proof} \begin{proposition}\label{strictorder_from_order} Suppose $R$ is an order. Then $\tostrictorder{R}$ is a strict order. \end{proposition} \begin{proof} - $\tostrictorder{R}$ is asymmetric. - $\tostrictorder{R}$ is transitive. + $\tostrictorder{R}$ is asymmetric + by \cref{antisymmetric,asymmetric,tostrictorder_iff}. + Show for all $a,b,c$ such that + $a\mathrel{\tostrictorder{R}}b$ and + $b\mathrel{\tostrictorder{R}}c$ + we have $a\mathrel{\tostrictorder{R}}c$. + \begin{subproof} + Fix $a,b,c$. + Assume $a\mathrel{\tostrictorder{R}}b$ and + $b\mathrel{\tostrictorder{R}}c$. + We have $a\mathrel{R}b$ and $b\mathrel{R}c$ + by \cref{tostrictorder_iff}. + Thus $a\mathrel{R}c$ by \cref{transitive}. + We have $a\neq c$ by \cref{asymmetric}. + Follows by \cref{tostrictorder_iff}. + \end{subproof} + Thus $\tostrictorder{R}$ is transitive by \cref{transitive}. + Follows by assumption. \end{proof} \begin{proposition}\label{order_from_strictorder} @@ -81,16 +103,42 @@ Then $\toorder{A}{R}$ is an order on $A$. \end{proposition} \begin{proof} - $\toorder{A}{R}$ is antisymmetric. + $\identity{A}\subseteq A\times A$ + by \cref{id_elem_rels,rels_elim}. + Thus $\toorder{A}{R}\subseteq A\times A$ + by \cref{toorder,union_subsets_is_subset}. + Hence $\toorder{A}{R}$ is a binary relation on $A$ + by assumption. + $\toorder{A}{R}$ is antisymmetric + by \cref{antisymmetric,asymmetric,toorder_iff}. $\toorder{A}{R}$ is transitive by \cref{transitive,toorder_iff}. - $\toorder{A}{R}$ is reflexive on $A$. + $\toorder{A}{R}$ is reflexive on $A$ by \cref{toorder_reflexive}. + Follows by assumption. \end{proof} \begin{proposition}\label{subseteqrel_antisymmetric} $\subseteqrel{A}$ is antisymmetric. \end{proposition} \begin{proof} - Follows by \cref{subseteqrel,antisymmetric,pair_eq_iff,subseteq_antisymmetric}. + Show for all $a,b$ such that + $a\mathrel{\subseteqrel{A}}b$ and + $b\mathrel{\subseteqrel{A}}a$ + we have $a=b$. + \begin{subproof} + Fix $a,b$. + Assume $a\mathrel{\subseteqrel{A}}b$ and + $b\mathrel{\subseteqrel{A}}a$. + Take $x,y$ such that $(a,b)=(x,y)$ and + $x,y\in A$ and $x\subseteq y$ by \cref{subseteqrel}. + Then $a=x$ and $b=y$ by \cref{pair_eq_iff}. + Thus $a\subseteq b$ by assumption. + Take $u,v$ such that $(b,a)=(u,v)$ and + $u,v\in A$ and $u\subseteq v$ by \cref{subseteqrel}. + Then $b=u$ and $a=v$ by \cref{pair_eq_iff}. + Thus $b\subseteq a$ by assumption. + Follows by \cref{subseteq_antisymmetric}. + \end{subproof} + Follows by \cref{antisymmetric}. \end{proof} @@ -100,4 +148,5 @@ \begin{proof} $\subseteqrel{A}$ is a quasiorder on $A$ by \cref{subseteqrel_is_quasiorder}. $\subseteqrel{A}$ is antisymmetric by \cref{subseteqrel_antisymmetric}. + Follows by assumption. \end{proof} diff --git a/library/order/quasiorder.tex b/library/order/quasiorder.tex index ab325e7..3ccb46e 100644 --- a/library/order/quasiorder.tex +++ b/library/order/quasiorder.tex @@ -37,15 +37,48 @@ Then $a\mathrel{\lt[X]} d$. \end{lemma} \begin{proof} - $\lt[X]$ is transitive. - Thus $a\mathrel{\lt[X]} c\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}. - Hence $a\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}. + $\lt[X]$ is transitive by \cref{quasiorder_tran}. + Thus $a\mathrel{\lt[X]} c\mathrel{\lt[X]} d$ by \cref{transitive}. + Hence $a\mathrel{\lt[X]} d$ by \cref{transitive}. + Follows by assumption. \end{proof} \begin{proposition}\label{subseteqrel_is_quasiorder} $\subseteqrel{A}$ is a quasiorder on $A$. \end{proposition} \begin{proof} - $\subseteqrel{A}$ is reflexive on $A$. - $\subseteqrel{A}$ is transitive. + Show for all $w\in\subseteqrel{A}$ we have $w\in A\times A$. + \begin{subproof} + Fix $w$. + Assume $w\in\subseteqrel{A}$. + Take $a,b$ such that $w=(a,b)$ and $a,b\in A$ + by \cref{subseteqrel,pair_eq_iff}. + Follows by \cref{times_tuple_intro}. + \end{subproof} + Thus $\subseteqrel{A}$ is a binary relation on $A$ + by \cref{subseteq}. + $\subseteqrel{A}$ is reflexive on $A$ + by \cref{reflexive_on,subseteqrel,subseteq}. + Show for all $a,b,c$ such that + $a\mathrel{\subseteqrel{A}}b$ and + $b\mathrel{\subseteqrel{A}}c$ + we have $a\mathrel{\subseteqrel{A}}c$. + \begin{subproof} + Fix $a,b,c$. + Assume $a\mathrel{\subseteqrel{A}}b$ and + $b\mathrel{\subseteqrel{A}}c$. + Take $x,y$ such that $(a,b)=(x,y)$ and + $x,y\in A$ and $x\subseteq y$ by \cref{subseteqrel}. + Then $a=x$ and $b=y$ by \cref{pair_eq_iff}. + Thus $a\subseteq b$ and $a\in A$ by assumption. + Take $u,v$ such that $(b,c)=(u,v)$ and + $u,v\in A$ and $u\subseteq v$ by \cref{subseteqrel}. + Then $b=u$ and $c=v$ by \cref{pair_eq_iff}. + Thus $b\subseteq c$ and $c\in A$ by assumption. + Thus $a\subseteq c$ by \cref{subseteq_transitive}. + Follows by \cref{subseteqrel}. + \end{subproof} + Thus $\subseteqrel{A}$ is transitive + by \cref{transitive}. + Follows by assumption. \end{proof} diff --git a/library/order/semilattice.tex b/library/order/semilattice.tex index 51af68b..76bbe56 100644 --- a/library/order/semilattice.tex +++ b/library/order/semilattice.tex @@ -1,7 +1,8 @@ -\import{order/partial-order.tex} +\import{order/order.tex} +\import{function.tex} \begin{struct}\label{meet_semilattice} - A meet semilattice $X$ is a partial order + A meet semilattice $X$ is an ordered set equipped with \begin{enumerate} \item $\meet$ @@ -9,7 +10,7 @@ such that \begin{enumerate} \item\label{meet_type} for all $x,y\in \carrier[X]$ we have - $\meet[X](x,y)\in X$. + $\meet[X](x,y)\in \carrier[X]$. \item\label{meet_lb} for all $x,y\in \carrier[X]$ we have $\meet[X](x,y) \mathrel{\lt[X]} x, y$. \item\label{meet_glb} for all $a,x,y\in \carrier[X]$ such that $a\mathrel{\lt[X]} x, y$ we have @@ -20,12 +21,16 @@ \begin{proposition}\label{meet_idempotent} Let $X$ be a meet semilattice. - Then $\meet(x,x) = x$. + Let $x\in\carrier[X]$. + Then $\meet[X](x,x) = x$. \end{proposition} \begin{proof} - $\meet(x,x) \mathrel{\lt} x$. - $x\mathrel{\lt[X]} x, x$. - Thus $x\mathrel{\lt[X]} \meet(x,x)$. + We have $\meet[X](x,x)\in\carrier[X]$ by \cref{meet_type}. + We have $\meet[X](x,x)\mathrel{\lt[X]}x$ by \cref{meet_lb}. + We have $x\mathrel{\lt[X]}x$ + by \cref{meet_semilattice,orderedset,quasiorder_refl,reflexive_on}. + Thus $x\mathrel{\lt[X]}\meet[X](x,x)$ by \cref{meet_glb}. + Follows by \cref{meet_semilattice,orderedset,orderedset_antisym,antisymmetric}. \end{proof} %\begin{proposition}\label{meet_comm} diff --git a/library/ordinal.tex b/library/ordinal.tex index f978257..f7a66d1 100644 --- a/library/ordinal.tex +++ b/library/ordinal.tex @@ -19,7 +19,7 @@ so we will explicitly talk about \emph{\in-transitivity} here. % \renewcommand{\in}{\ensuremath{\mathonlyin}} % \begin{definition}\label{transitiveset} - A set $A$ is \in-transitive iff for all $x, y$ + $A$ is \in-transitive iff for all $x, y$ such that $x\in y\in A$ we have $x\in A$. \end{definition} @@ -27,12 +27,16 @@ so we will explicitly talk about \emph{\in-transitivity} here. $A$ is \in-transitive iff for all $a\in A$ we have $a\subseteq A$. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,subseteq}. +\end{proof} \begin{proposition}\label{transitiveset_iff_pow} $A$ is \in-transitive iff $A\subseteq \pow{A}$. \end{proposition} \begin{proof} - For all $a\in A$ we have $a\subseteq A \iff a\in\pow{A}$. + For all $a\in A$ we have $a\subseteq A \iff a\in\pow{A}$ + by \cref{subseteq,pow_iff}. Follows by \cref{elem_subseteq,subseteq,pow_iff,transitiveset_iff_subseteq}. \end{proof} @@ -40,18 +44,28 @@ so we will explicitly talk about \emph{\in-transitivity} here. $A$ is \in-transitive iff $\unions{\suc{A}} = A$. \end{proposition} \begin{proof} - Follows by \cref{transitiveset,subseteq,subseteq_antisymmetric,suc,transitiveset_iff_pow,unions_subseteq_of_powerset_is_subseteq,unions_iff,suc_subseteq_intro,powerset_top}. + We have if $A$ is \in-transitive, then $\unions{\suc{A}}=A$ + by \cref{setext,transitiveset,unions_iff,suc_iff}. + We have if $\unions{\suc{A}}=A$, then $A$ is \in-transitive + by \cref{transitiveset,unions_iff,suc_iff}. + Follows by assumption. \end{proof} \begin{proposition}\label{transitiveset_iff_unions_subseteq} $A$ is \in-transitive iff $\unions{A}\subseteq A$. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,subseteq,unions_iff}. +\end{proof} \begin{proposition}\label{transitiveset_upair} Suppose $A$ is \in-transitive. Suppose $\{a,b\}\in A$. Then $a,b\in A$. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,transitiveset_iff_subseteq,subseteq}. +\end{proof} % For Kuratowski pairs only: %\begin{proposition}\label{transitiveset_pair} @@ -81,26 +95,41 @@ so we will explicitly talk about \emph{\in-transitivity} here. \begin{proposition}\label{emptyset_transitiveset} $\emptyset$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,emptyset}. +\end{proof} \begin{proposition}\label{union_of_transitiveset_is_transitiveset} Suppose $A$ and $B$ are \in-transitive. Then $A\union B$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,union_iff}. +\end{proof} \begin{proposition}\label{inter_of_transitiveset_is_transitiveset} Let $A, B$ be \in-transitive sets. Then $A\inter B$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,inter}. +\end{proof} \begin{proposition}\label{suc_of_transitiveset_is_transitiveset} Let $A$ be an \in-transitive set. Then $\suc{A}$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,suc}. +\end{proof} \begin{proposition}\label{unions_of_transitiveset_is_transitiveset} Let $A$ be an \in-transitive set. Then $\unions{A}$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,unions_iff}. +\end{proof} \begin{proposition}\label{unions_family_of_transitiveset_is_transitiveset} Suppose every element of $A$ is an \in-transitive set. @@ -132,28 +161,43 @@ so we will explicitly talk about \emph{\in-transitivity} here. Suppose every element of $\alpha$ is \in-transitive. Then $\alpha$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal}. +\end{proof} \begin{proposition}\label{ordinal_is_transitiveset} Let $\alpha$ be an ordinal. Then $\alpha$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{ordinal}. +\end{proof} \begin{proposition}\label{ordinal_elem_is_transitiveset} Let $\alpha$ be an ordinal. Suppose $A\in\alpha$. Then $A$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{ordinal}. +\end{proof} \begin{proposition}\label{elem_of_ordinal_is_ordinal} Let $\alpha$ be an ordinal. Suppose $\beta\in\alpha$. Then $\beta$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,transitiveset}. +\end{proof} \begin{proposition}\label{suc_ordinal_implies_ordinal} Suppose $\suc{\alpha}$ is an ordinal. Then $\alpha$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,suc}. +\end{proof} \begin{proposition}\label{transitivesubseteq_of_ordinal_is_ordinal} Let $\alpha$ be an ordinal. @@ -170,6 +214,9 @@ so we will explicitly talk about \emph{\in-transitivity} here. Suppose $\alpha\in\beta$. Then $\alpha\subseteq\beta$. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,transitiveset_iff_subseteq}. +\end{proof} \begin{proposition}\label{ordinal_transitivity} Let $\alpha$ be an ordinal. @@ -186,6 +233,9 @@ so we will explicitly talk about \emph{\in-transitivity} here. Suppose $\alpha\in\beta$. Then $\suc{\alpha}\subseteq\beta$. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,transitiveset_iff_subseteq,suc_subseteq_intro}. +\end{proof} \begin{abbreviation}\label{ordinal_prec} @@ -217,26 +267,42 @@ We already have global irreflexivity and asymmetry of \in. \in\ is transitive on ordinals by definition. To show that \in\ is a strict total order it only remains to show that \in\ is connex. +\begin{lemma}\label{ordinal_elem_connex_from_elements} + Let $\alpha,\gamma$ be ordinals. + Suppose for all sets $\xi,\beta$ such that $\xi\in\alpha$ and $\beta$ is an ordinal + we have $\xi\in\beta\lor \beta\in\xi \lor \xi = \beta$. + Suppose for every $\eta\in\gamma$ + we have $\alpha\in\eta\lor \eta\in\alpha \lor \alpha = \eta$. + Then $\alpha\in\gamma\lor \gamma\in\alpha \lor \alpha = \gamma$. +\end{lemma} +\begin{proof} + Assume neither $\alpha\in\gamma$ nor $\gamma\in\alpha$. + For every $\xi\in\alpha$ we have $\xi\in\gamma$ + by \cref{ordinal_transitivity}. + Thus $\alpha\subseteq\gamma$ by \cref{subseteq}. + For every $\eta\in\gamma$ we have $\eta\in\alpha$ + by \cref{ordinal_transitivity}. + Thus $\gamma\subseteq\alpha$ by \cref{subseteq}. + Follows by \cref{subseteq_antisymmetric}. +\end{proof} + +\begin{lemma}\label{ordinal_elem_connex_step} + Let $\alpha,\gamma$ be ordinals. + Suppose for all sets $\xi,\beta$ such that $\xi\in\alpha$ and $\beta$ is an ordinal + we have $\xi\in\beta\lor \beta\in\xi \lor \xi = \beta$. + Then $\alpha\in\gamma\lor \gamma\in\alpha \lor \alpha = \gamma$. +\end{lemma} +\begin{proof}[Proof by \in-induction on $\gamma$] + Follows by \cref{ordinal_elem_connex_from_elements,elem_of_ordinal_is_ordinal}. +\end{proof} + \begin{proposition}\label{ordinal_elem_connex} - For all ordinals $\alpha,\beta$ + Let $\alpha$ be an ordinal. + Then for every ordinal $\beta$ we have $\alpha\in\beta\lor \beta\in\alpha \lor \alpha = \beta$. \end{proposition} \begin{proof}[Proof by \in-induction on $\alpha$] - % Ind hypothesis: - % ![Xi,Xbeta]:(elem(Xi,falpha)=>((ordinal(Xi)&ordinal(Xbeta))=>(elem(Xi,Xbeta)|elem(Xbeta,Xi)|Xi=Xbeta)))) - % Goal: - % ordinal(falpha)&ordinal(fbeta))=>(elem(falpha,fbeta)|elem(fbeta,falpha)|falpha=fbeta) - % - Assume $\alpha$ is an ordinal. - Show for all ordinals $\gamma$ we have $\alpha\in\gamma\lor \gamma\in\alpha \lor \alpha = \gamma$. - \begin{subproof}[Proof by \in-induction on $\gamma$] - % Now we have: - % ![Xi]:(elem(Xi,fgamma)=>(ordinal(Xi)=>(elem(falpha,Xi)|elem(Xi,falpha)|falpha=Xi)))). - % Goal: ordinal(fgamma)=>(elem(falpha,fgamma)|elem(fgamma,falpha)|falpha=fgamma)) - % - Assume $\gamma$ is an ordinal. - Follows by \cref{setext,transitiveset,ordinal}. - \end{subproof} + Follows by \cref{ordinal_elem_connex_step,elem_of_ordinal_is_ordinal}. \end{proof} \begin{proposition}\label{ordinal_proper_subset_implies_elem} @@ -245,20 +311,24 @@ To show that \in\ is a strict total order it only remains to show that \in\ is c Then $\alpha\in\beta$. \end{proposition} \begin{proof} - $\beta\setminus\alpha$ is inhabited. - Take $\gamma$ such that $\gamma$ is an \in-minimal element of $\beta\setminus\alpha$. + $\beta\setminus\alpha$ is inhabited + by \cref{difference_with_proper_subset_is_inhabited}. + Take $\gamma$ such that $\gamma$ is an \in-minimal element of $\beta\setminus\alpha$ + by \cref{regularity}. Now $\gamma\in\beta$ by \cref{setminus_elim_left}. - Hence $\gamma\subseteq\beta$ - by \cref{ordinal,transitiveset_iff_subseteq}. - For all $\delta\in\beta\setminus\alpha$ we have $\delta\notin\gamma$. - Thus $\gamma\setminus\alpha = \emptyset$. - Hence $\gamma\subseteq\alpha$. - It suffices to show that for all $\delta\in\alpha$ we have $\delta\in\gamma$. - Suppose not. - Take $\delta\in\alpha$ such that $\delta\notin\gamma$. - Now if $\delta = \gamma$ or $\gamma\in\delta$, then $\gamma\in\alpha$ - % Original Vampire proof: by \cref{ordinal,elem_subseteq,elem_of_ordinal_is_ordinal,setminus_elim_left,ordinal_elem_connex,inter_eq_left_implies_subseteq,inter_absorb_supseteq_left,transitiveset_iff_subseteq}. - by \cref{ordinal,elem_subseteq,elem_of_ordinal_is_ordinal,ordinal_elem_connex,transitiveset_iff_subseteq}. + Thus $\gamma$ is an ordinal by \cref{elem_of_ordinal_is_ordinal}. + Hence $\gamma\subseteq\beta$ by \cref{ordinal_elem_implies_subseteq}. + For all $\delta\in\beta\setminus\alpha$ we have $\delta\notin\gamma$ + by \cref{disjoint}. + Thus $\gamma\setminus\alpha = \emptyset$ + by \cref{setext,setminus_intro,setminus_elim_left,setminus_elim_right,elem_subseteq}. + Hence $\gamma\subseteq\alpha$ + by \cref{setminus_eq_emptyset_iff_subseteq}. + For all $\delta\in\alpha$ we have $\delta\in\gamma$ + by \cref{ordinal_elem_connex,ordinal_is_transitiveset,elem_of_ordinal_is_ordinal,transitiveset_iff_subseteq,elem_subseteq,setminus_elim_right}. + Thus $\alpha\subseteq\gamma$ by \cref{subseteq}. + Thus $\alpha = \gamma$ by \cref{subseteq_antisymmetric}. + Follows by assumption. \end{proof} \begin{proposition}\label{ordinal_elem_implies_proper_subset} @@ -267,7 +337,7 @@ To show that \in\ is a strict total order it only remains to show that \in\ is c Then $\alpha\subset\beta$. \end{proposition} \begin{proof} - $\alpha\subseteq\beta$. + Follows by \cref{subset,ordinal_elem_implies_subseteq,in_irrefl}. \end{proof} \begin{proposition}\label{ordinal_preceq_implies_subseteq} @@ -276,12 +346,7 @@ Suppose $\alpha\precedeseq\beta$. Then $\alpha\subseteq\beta$. \end{proposition} \begin{proof} - \begin{byCase} - \caseOf{$\alpha = \beta$.} - Trivial. - \caseOf{$\alpha\precedes\beta$.} - $\alpha\subset\beta$. - \end{byCase} + Follows by assumption. \end{proof} %\begin{proposition}% @@ -304,12 +369,18 @@ Then $\alpha\subseteq\beta$. Let $\alpha,\beta$ be ordinals. Then $\alpha\in\beta$ or $\beta\subseteq\alpha$. \end{proposition} +\begin{proof} + Follows by \cref{ordinal_elem_connex,ordinal_elem_implies_subseteq,subseteq}. +\end{proof} \begin{proposition}\label{ordinal_subseteq_or_subseteq} Let $\alpha,\beta$ be ordinals. Then $\alpha\subseteq\beta$ or $\beta\subseteq\alpha$. \end{proposition} +\begin{proof} + Follows by \cref{ordinal_elem_connex,ordinal_elem_implies_subseteq,subseteq}. +\end{proof} \begin{proposition}\label{ordinal_subseteq_implies_elem_or_eq} @@ -317,12 +388,18 @@ Then $\alpha\subseteq\beta$. Suppose $\alpha\subseteq\beta$. Then $\alpha\in\beta$ or $\alpha = \beta$. \end{proposition} +\begin{proof} + Follows by \cref{subset,ordinal_proper_subset_implies_elem}. +\end{proof} \begin{corollary}\label{ordinal_subset_trichotomy} Let $\alpha,\beta$ be ordinals. Then $(\alpha\subset\beta \lor \beta\subset\alpha) \lor \alpha = \beta$. \end{corollary} +\begin{proof} + Follows by \cref{subset,ordinal_elem_connex,ordinal_elem_implies_proper_subset}. +\end{proof} \begin{proposition}\label{ordinal_nor_elem_implies_eq} Let $\alpha,\beta$ be ordinals. @@ -330,16 +407,14 @@ Then $\alpha\subseteq\beta$. Then $\alpha = \beta$. \end{proposition} \begin{proof} - Neither $\alpha\subset\beta$ nor $\beta\subset\alpha$. + Follows by \cref{ordinal_elem_connex}. \end{proof} \begin{proposition}\label{ordinal_in_trichotomy} Let $\alpha,\beta$ be ordinals. Then $(\alpha\in\beta \lor \beta\in\alpha) \lor \alpha = \beta$. \end{proposition} \begin{proof} - Suppose not. - Then neither $\alpha\in\beta$ nor $\beta\in\alpha$. - Thus $\alpha = \beta$ by \cref{ordinal_nor_elem_implies_eq}. Contradiction. + Follows by \cref{ordinal_elem_connex}. \end{proof} \begin{corollary}\label{ordinal_prec_trichotomy} @@ -354,6 +429,9 @@ Then $\alpha\subseteq\beta$. \begin{corollary}\label{ordinal_elem_or_superset} Let $\alpha,\beta$ be ordinals. Then $\alpha\in \beta$ or $\beta\subseteq \alpha$. \end{corollary} +\begin{proof} + Follows by \cref{ordinal_elem_or_subseteq}. +\end{proof} @@ -362,6 +440,9 @@ Then $\alpha\subseteq\beta$. \begin{proposition}\label{emptyset_is_ordinal} $\emptyset$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,transitiveset,emptyset}. +\end{proof} % The proof of this theorem benefits from the alternate definition of % transitivity in terms of $\subseteq$. @@ -371,22 +452,33 @@ Then $\alpha\subseteq\beta$. \end{proposition} \begin{proof} $\suc{\alpha}$ is \in-transitive by \cref{ordinal,suc_of_transitiveset_is_transitiveset}. - For every $\beta\in\alpha$ we have that $\beta$ is \in-transitive. + For every $\beta\in\alpha$ we have that $\beta$ is \in-transitive + by \cref{ordinal,transitiveset}. + Follows by \cref{ordinal,suc_iff}. \end{proof} \begin{proposition}\label{ordinal_iff_suc_ordinal} $\alpha$ is an ordinal iff $\suc{\alpha}$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{suc_ordinal,suc_intro_self,elem_of_ordinal_is_ordinal}. +\end{proof} \begin{proposition}\label{ordinal_in_suc} Let $\alpha$ be an ordinal. Then $\alpha\in\suc{\alpha}$. \end{proposition} +\begin{proof} + Follows by \cref{suc_intro_self}. +\end{proof} \begin{corollary}\label{ordinal_precedes_suc} Let $\alpha$ be an ordinal. Then $\alpha\precedes \suc{\alpha}$. \end{corollary} +\begin{proof} + Follows by \cref{suc_ordinal,ordinal_in_suc}. +\end{proof} \begin{proposition}\label{ordinal_elem_implies_subset_of_suc} Let $\alpha,\beta$ be ordinals. @@ -394,9 +486,7 @@ Then $\alpha\subseteq\beta$. Then $\alpha\subseteq\suc{\beta}$. \end{proposition} \begin{proof} - $\alpha\subset \beta$. - In particular, $\alpha\subseteq \beta$. - Hence $\alpha\subseteq \cons{\beta}{\beta}$. + Follows by \cref{ordinal_elem_implies_subseteq,subseteq_self_suc_intro,subseteq_transitive}. \end{proof} \begin{proposition}\label{unions_of_ordinal_is_ordinal} @@ -406,8 +496,10 @@ Then $\alpha\subseteq\beta$. \begin{proof} For all $x, y$ such that $x\in y\in \unions{\alpha}$ we have $x\in \unions{\alpha}$ by \cref{unions_intro,unions_iff,transitiveset,ordinal}. - Thus $\unions{\alpha}$ is \in-transitive. - Every element of $\unions{\alpha}$ is \in-transitive. + Thus $\unions{\alpha}$ is \in-transitive by \cref{transitiveset}. + Every element of $\unions{\alpha}$ is \in-transitive + by \cref{unions_iff,ordinal,transitiveset}. + Follows by \cref{ordinal}. \end{proof} \begin{lemma}\label{ordinal_subseteq_unions} @@ -430,11 +522,11 @@ Then $\alpha\subseteq\beta$. \end{proof} \begin{proposition}\label{ordinal_empty_or_emptyset_elem} - For all ordinals $\alpha$ - we have $\alpha=\emptyset$ or $\emptyset\in\alpha$. + Let $\alpha$ be an ordinal. + Then $\alpha=\emptyset$ or $\emptyset\in\alpha$. \end{proposition} -\begin{proof}[Proof by \in-induction] - Straightforward. +\begin{proof}[Proof by \in-induction on $\alpha$] + Follows by \cref{setext,emptyset,elem_of_ordinal_is_ordinal,ordinal_transitivity}. \end{proof} \begin{proposition}\label{transitive_set_of_ordinals_is_ordinal} @@ -443,6 +535,9 @@ Then $\alpha\subseteq\beta$. Suppose that $A$ is \in-transitive. Then $A$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal}. +\end{proof} % Apparently Russel first noticed this antimony while reading a paper by Burali-Forti. % Typographic NB: Cesare Burali-Forti is a single person, therefore only a single hyphen! @@ -451,13 +546,17 @@ Then $\alpha\subseteq\beta$. for all $\alpha$ we have $\alpha\in \Omega$ iff $\alpha$ is an ordinal. \end{theorem} \begin{proof} - Suppose not. - Take $\Omega$ such that for all $\alpha$ we have $\alpha\in \Omega$ iff $\alpha$ is an ordinal. - For all $x, y$ such that $x\in y\in \Omega$ we have $x\in \Omega$. - Thus $\Omega$ is \in-transitive. - Thus $\Omega$ is an ordinal. - Therefore $\Omega\in\Omega$. - Contradiction. + Assume there exists a set $\Omega$ such that + for all $\alpha$ we have $\alpha\in \Omega$ iff $\alpha$ is an ordinal. + Take $\Omega$ such that for all $\alpha$ we have + $\alpha\in \Omega$ iff $\alpha$ is an ordinal by assumption. + For all $x, y$ such that $x\in y\in \Omega$ we have $x\in \Omega$ + by \cref{elem_of_ordinal_is_ordinal}. + Thus $\Omega$ is \in-transitive by \cref{transitiveset}. + For every $\alpha\in\Omega$ we have $\alpha$ is an ordinal by assumption. + Thus $\Omega$ is an ordinal by \cref{ordinal}. + Therefore $\Omega\in\Omega$ by assumption. + Contradiction by \cref{in_irrefl}. \end{proof} \begin{proposition}\label{inters_of_ordinals_is_ordinal} @@ -466,7 +565,13 @@ Then $\alpha\subseteq\beta$. Then $\inters{A}$ is an ordinal. \end{proposition} \begin{proof} - It suffices to show that $\inters{A}$ is \in-transitive. + For all $x,y$ such that $x\in y\in\inters{A}$ we have $x\in\inters{A}$ + by \cref{inters_iff_forall,ordinal_transitivity}. + Thus $\inters{A}$ is \in-transitive by \cref{transitiveset}. + Take $\alpha$ such that $\alpha\in A$ by assumption. + For every $y\in\inters{A}$ we have $y$ is an ordinal + by \cref{inters_iff_forall,elem_of_ordinal_is_ordinal}. + Follows by \cref{ordinal}. \end{proof} \begin{proposition}\label{inters_of_ordinals_subseteq} @@ -474,6 +579,9 @@ Then $\alpha\subseteq\beta$. Suppose for every $\alpha\in A$ we have $\alpha$ is an ordinal. Then for all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$. \end{proposition} +\begin{proof} + Follows by \cref{inters_subseteq_elem}. +\end{proof} \begin{proposition}\label{inters_of_ordinals_elem} Let $A$ be an inhabited set. @@ -491,7 +599,12 @@ Then $\alpha\subseteq\beta$. Then $\inters{A}$ is an \in-minimal element of $A$. \end{proposition} \begin{proof} - For all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$. + $\inters{A}\in A$ by \cref{inters_of_ordinals_elem}. + For all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$ + by \cref{inters_of_ordinals_subseteq}. + For all $\delta\in\inters{A}$ we have $\delta\notin A$ + by \cref{elem_of_ordinal_is_ordinal,ordinal_elem_implies_proper_subset,subset,subseteq_antisymmetric}. + Follows by \cref{disjoint}. \end{proof} \begin{proposition}\label{inters_of_ordinals_is_minimal_alternate} @@ -500,7 +613,7 @@ Then $\alpha\subseteq\beta$. Then for all $\alpha\in A$ we have $\inters{A} = \alpha$ or $\inters{A}\in\alpha$. \end{proposition} \begin{proof} - For all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$. + Follows by \cref{inters_of_ordinals_is_ordinal,inters_of_ordinals_subseteq,ordinal_subseteq_implies_elem_or_eq}. \end{proof} \begin{proposition}\label{inter_of_two_ordinals_is_ordinal} @@ -534,27 +647,28 @@ Then $\alpha\subseteq\beta$. Then $\alpha$ is a limit ordinal or $\alpha$ is a successor ordinal. \end{lemma} \begin{proof} - \begin{byCase} - \caseOf{$\alpha$ is a limit ordinal.} - Trivial. - \caseOf{$\alpha$ is not a limit ordinal.} - Take $\beta$ such that $\beta\in\alpha$ and $\suc{\beta}\notin\alpha$ - by \cref{limit_ordinal}. - \end{byCase} + Assume $\alpha$ is not a limit ordinal. + Take $\beta$ such that $\beta\in\alpha$ and $\suc{\beta}\notin\alpha$ + by \cref{limit_ordinal}. + Thus $\beta$ is an ordinal by \cref{elem_of_ordinal_is_ordinal}. + Thus $\suc{\beta}$ is an ordinal by \cref{suc_ordinal}. + We have $\alpha=\suc{\beta}$ + by \cref{ordinal_elem_connex,suc_elim,in_asymmetric,in_irrefl}. + Follows by \cref{successor_ordinal}. \end{proof} \begin{lemma}\label{zero_not_successorordinal} $\emptyset$ is not a successor ordinal. \end{lemma} +\begin{proof} + Follows by \cref{successor_ordinal,suc_neq_emptyset}. +\end{proof} \begin{lemma}\label{zero_not_limitordinal} $\emptyset$ is not a limit ordinal. \end{lemma} \begin{proof} - Suppose not. - Then $\emptyset\precedes \emptyset$ by \cref{emptyset,limit_ordinal}. - Thus $\emptyset\in \emptyset$. - Contradiction. + Follows by \cref{limit_ordinal,emptyset,in_irrefl}. \end{proof} \begin{lemma}\label{suc_elem_limitordinal} diff --git a/library/relation/closure.tex b/library/relation/closure.tex index 8eebf08..0734685 100644 --- a/library/relation/closure.tex +++ b/library/relation/closure.tex @@ -11,6 +11,9 @@ \begin{proposition}\label{reflexive_closure_is_reflexive} $\reflexiveClosure{X}{R}$ is reflexive on $X$. \end{proposition} +\begin{proof} + Follows by \cref{reflexive_closure,reflexive_on,union_iff,id_iff}. +\end{proof} \begin{definition}\label{reflexive_reduction} $\reflexiveReduction{X}{R} = R\setminus\identity{X}$. diff --git a/library/relation/equivalence.tex b/library/relation/equivalence.tex index f8b1ba7..896ca57 100644 --- a/library/relation/equivalence.tex +++ b/library/relation/equivalence.tex @@ -16,6 +16,9 @@ Let $E$ be a partial equivalence. Then $E$ is quasireflexive. \end{proposition} +\begin{proof} + Follows by \cref{quasireflexive,symmetric,transitive}. +\end{proof} \begin{abbreviation}\label{equivalence} $E$ is an equivalence iff @@ -88,6 +91,12 @@ Then $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$. \end{proposition} \begin{proof} + We have for all $c\in\equivalenceClass{E}{a}$ + we have $c\in\equivalenceClass{E}{b}$ + by \cref{downward_closure_iff,transitive}. + We have for all $c\in\equivalenceClass{E}{b}$ + we have $c\in\equivalenceClass{E}{a}$ + by \cref{downward_closure_iff,symmetric,transitive}. Follows by set extensionality. \end{proof} @@ -97,12 +106,20 @@ Suppose $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$. Then $a\mathrel{E} b$. \end{proposition} +\begin{proof} + $a\in\equivalenceClass{E}{a}$ by \cref{equivclasses_inhabited_equivalenceon}. + Thus $a\in\equivalenceClass{E}{b}$. + Follows by \cref{downward_closure_iff}. +\end{proof} \begin{proposition}\label{equiv_iff_equivclasses_eq} Let $E$ be an equivalence on $A$. Let $a, b\in A$. Then $a\mathrel{E} b$ iff $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$. \end{proposition} +\begin{proof} + Follows by \cref{equiv_implies_equivanlence_classes_eq,equivclasses_eq_implies_equiv}. +\end{proof} \begin{proposition}\label{equivclasses_diseq_implies_disjoint} Let $E$ be a partial equivalence. @@ -110,21 +127,28 @@ Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$. \end{proposition} \begin{proof} - Suppose not. - Take $c$ such that $c\in \equivalenceClass{E}{a},\equivalenceClass{E}{b}$. - Then $c\mathrel{E} a$ and - $c\mathrel{E} b$. - $E$ is symmetric. - Thus $a\mathrel{E} c$ by \hyperref[symmetric]{symmetry}. - $E$ is transitive. - Thus $a\mathrel{E} b$ by \hyperref[transitive]{transitivity}. - Then $b\mathrel{E} a$ by \hyperref[symmetric]{symmetry}. - % - Thus $a\in \equivalenceClass{E}{b}$ and $b\in \equivalenceClass{E}{a}$ - by \cref{downward_closure_iff}. - Hence $\equivalenceClass{E}{a}\subseteq \equivalenceClass{E}{b}\subseteq \equivalenceClass{E}{a}$ - by \cref{transitive_downward_subseteq}. - Contradiction by \cref{subseteq_antisymmetric}. + Show there exists no $c$ such that + $c\in\equivalenceClass{E}{a}$ and + $c\in\equivalenceClass{E}{b}$. + \begin{subproof} + Assume there exists a set $c$ such that + $c\in\equivalenceClass{E}{a}$ and + $c\in\equivalenceClass{E}{b}$. + Take $c$ such that $c\in\equivalenceClass{E}{a}$ and + $c\in\equivalenceClass{E}{b}$ by assumption. + We have $c\mathrel{E}a$ and $c\mathrel{E}b$ + by \cref{downward_closure_iff}. + Thus $a\mathrel{E}c$ and $b\mathrel{E}c$ by \cref{symmetric}. + Thus $a\mathrel{E}b$ and $b\mathrel{E}a$ by \cref{transitive}. + Hence $\equivalenceClass{E}{a}\subseteq\equivalenceClass{E}{b}$ + by \cref{downward_closure_iff,transitive_downward_subseteq}. + We have $\equivalenceClass{E}{b}\subseteq\equivalenceClass{E}{a}$ + by \cref{downward_closure_iff,transitive_downward_subseteq}. + Thus $\equivalenceClass{E}{a}=\equivalenceClass{E}{b}$ + by \cref{subseteq_antisymmetric}. + Contradiction by assumption. + \end{subproof} + Follows by \cref{disjoint}. \end{proof} \begin{corollary}\label{equivalence_equivclasses_diseq_implies_disjoint} @@ -159,6 +183,13 @@ \begin{proposition}\label{quotient_emptyset} $\quotient{\emptyset}{\emptyset} = \emptyset$. \end{proposition} +\begin{proof} + We have for all $C\in\quotient{\emptyset}{\emptyset}$ + we have $C\in\emptyset$ by \cref{quotient,emptyset}. + We have for all $C\in\emptyset$ + we have $C\in\quotient{\emptyset}{\emptyset}$ by \cref{emptyset}. + Follows by set extensionality. +\end{proof} \begin{proposition}\label{quotient_elems_disjoint} @@ -167,8 +198,8 @@ Then $B$ is disjoint from $C$. \end{proposition} \begin{proof} - Take $b$ such that $B = \equivalenceClass{E}{b}$. - Take $c$ such that $C = \equivalenceClass{E}{c}$. + Take $b$ such that $b\in A$ and $B = \equivalenceClass{E}{b}$ by \cref{quotient}. + Take $c$ such that $c\in A$ and $C = \equivalenceClass{E}{c}$ by \cref{quotient}. Then $B$ is disjoint from $C$ by \cref{equivalenceon_equivclasses_diseq_implies_disjoint}. \end{proof} @@ -178,8 +209,8 @@ Then $C$ is inhabited. \end{proposition} \begin{proof} - Take $a\in A$ such that $C = \equivalenceClass{E}{a}$. - Then $a\in \equivalenceClass{E}{a}$. + Take $a$ such that $a\in A$ and $C = \equivalenceClass{E}{a}$ by \cref{quotient}. + Then $a\in \equivalenceClass{E}{a}$ by \cref{equivclasses_inhabited_equivalenceon}. $C$ is inhabited by \cref{quotient,equivclasses_inhabited}. \end{proof} @@ -189,7 +220,7 @@ Then $a\in A$. \end{proposition} \begin{proof} - Take $b\in A$ such that $C = \equivalenceClass{E}{b}$ + Take $b$ such that $b\in A$ and $C = \equivalenceClass{E}{b}$ by \cref{quotient}. Then $a\mathrel{E} b$. Thus $a\in A$ by \cref{times_tuple_elim,subseteq}. @@ -200,14 +231,19 @@ Let $E$ be an equivalence on $A$. $\emptyset\notin\quotient{A}{E}$. \end{corollary} +\begin{proof} + Follows by \cref{quotient_elems_inhabited,emptyset}. +\end{proof} \begin{proposition}\label{quotient_partition} Let $E$ be an equivalence on $A$. $\quotient{A}{E}$ is a partition. \end{proposition} \begin{proof} - $\emptyset\notin\quotient{A}{E}$. - For all $B, C\in \quotient{A}{E}$ such that $B\neq C$ we have $B$ is disjoint from $C$. + $\emptyset\notin\quotient{A}{E}$ by \cref{quotient_notni_emptyset}. + For all $B, C\in \quotient{A}{E}$ such that $B\neq C$ + we have $B$ is disjoint from $C$ by \cref{quotient_elems_disjoint}. + Follows by \cref{partition}. \end{proof} \begin{proposition}\label{quotient_partition_of} @@ -215,7 +251,13 @@ $\quotient{A}{E}$ is a partition of $A$. \end{proposition} \begin{proof} - $\unions{(\quotient{A}{E})} = A$ by set extensionality. + We have for all $a\in\unions{(\quotient{A}{E})}$ + we have $a\in A$ by \cref{unions_iff,quotient_elems_type}. + We have for all $a\in A$ + we have $a\in\unions{(\quotient{A}{E})}$ + by \cref{unions_iff,quotient,equivclasses_inhabited_equivalenceon}. + Thus $\unions{(\quotient{A}{E})} = A$ by set extensionality. + Follows by \cref{quotient_partition}. \end{proof} @@ -230,11 +272,17 @@ Suppose $a,b\in C\in P$. Then $a\mathrel{\equivfrompartition{P}{A}} b$. \end{proposition} +\begin{proof} + Follows by \cref{equivalence_from_partition}. +\end{proof} \begin{proposition}\label{equivalence_from_partition_reflexive} Let $P$ be a partition of $A$. $\equivfrompartition{P}{A}$ is reflexive on $A$. \end{proposition} +\begin{proof} + Follows by \cref{reflexive_on,equivalence_from_partition_intro,partition,unions_iff}. +\end{proof} \begin{proposition}\label{equivalence_from_partition_symmetric} Let $P$ be a partition. diff --git a/library/set.tex b/library/set.tex index 2df4768..d0cbb97 100644 --- a/library/set.tex +++ b/library/set.tex @@ -898,13 +898,25 @@ The $\operatorname{\textsf{cons}}$ operation is set adjunction. $A\setminus \cons{a}{B} = (A\setminus \{a\})\setminus B$. \end{proposition} \begin{proof} - Follows by \cref{cons_iff,setext,setminus}. + We have for all $x\in A\setminus \cons{a}{B}$ we have + $x\in (A\setminus \{a\})\setminus B$ + by \cref{cons_iff,setminus}. + We have for all $x\in (A\setminus \{a\})\setminus B$ we have + $x\in A\setminus \cons{a}{B}$ + by \cref{cons_iff,setminus}. + Follows by set extensionality. \end{proof} \begin{proposition}\label{setminus_cons_flip} $A\setminus \cons{a}{B} = (A\setminus B)\setminus \{a\}$. \end{proposition} \begin{proof} - Follows by \cref{cons_iff,setext,setminus}. + We have for all $x\in A\setminus \cons{a}{B}$ we have + $x\in (A\setminus B)\setminus \{a\}$ + by \cref{cons_iff,setminus}. + We have for all $x\in (A\setminus B)\setminus \{a\}$ we have + $x\in A\setminus \cons{a}{B}$ + by \cref{cons_iff,setminus}. + Follows by set extensionality. \end{proof} \begin{proposition}\label{setminus_disjoint} diff --git a/library/set/cons.tex b/library/set/cons.tex index 5972ebe..4ab1041 100644 --- a/library/set/cons.tex +++ b/library/set/cons.tex @@ -111,7 +111,11 @@ Then $\cons{a}{A\setminus\{a\}} = A$. \end{proposition} \begin{proof} - Follows by \cref{cons_iff,setext,setminus}. + We have for all $x\in\cons{a}{A\setminus\{a\}}$ we have $x\in A$ + by \cref{cons_iff,setminus}. + We have for all $x\in A$ we have $x\in\cons{a}{A\setminus\{a\}}$ + by \cref{cons_iff,setminus}. + Follows by set extensionality. \end{proof} \begin{proposition}\label{cons_idempotent} diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex index a922052..7c12d7a 100644 --- a/library/set/equinumerosity.tex +++ b/library/set/equinumerosity.tex @@ -15,7 +15,7 @@ $A\approx A$. \end{proposition} \begin{proof} - $\identity{A}$ is a bijection from $A$ to $A$. %by \cref{id_is_bijection}. + $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_elem_bijections}. Follows by \cref{equinum}. \end{proof} @@ -23,7 +23,7 @@ Suppose $A\approx B$. Then $B\approx A$. \end{proposition} \begin{proof} - Take a bijection $f$ from $A$ to $B$ by \cref{equinum}. + Take $f$ such that $f$ is a bijection from $A$ to $B$ by \cref{equinum}. Then $\converse{f}$ is a bijection from $B$ to $A$ by \cref{bijection_converse_is_bijection}. Follows by \cref{equinum}. \end{proof} @@ -32,8 +32,8 @@ Suppose $A\approx B\approx C$. Then $A\approx C$. \end{proposition} \begin{proof} - Take a bijection $f$ from $A$ to $B$ by \cref{equinum}. - Take a bijection $g$ from $B$ to $C$ by \cref{equinum}. + Take $f$ such that $f$ is a bijection from $A$ to $B$ by \cref{equinum}. + Take $g$ such that $g$ is a bijection from $B$ to $C$ by \cref{equinum}. Then $g\circ f$ is a bijection from $A$ to $C$ by \cref{bijection_circ}. Follows by \cref{equinum}. \end{proof} @@ -46,16 +46,33 @@ Then $A\approx B$. \end{theorem} \begin{proof} + For all $X\in\pow{A}$ we have + $A\setminus \img{g}{B\setminus\img{f}{X}}\subseteq A$ + by \cref{setminus_subseteq}. + For all $X\in\pow{A}$ we have + $A\setminus \img{g}{B\setminus\img{f}{X}}\in\pow{A}$ + by \cref{powerset_intro}. Let $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ for $X\in\pow{A}$. - %By construction: $h$ is a relation. - %By construction: $h$ is right-unique. - %By construction: $\dom{h} = \pow{A}$. - For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by \cref{setminus_subseteq,pow_iff}. - Thus $h$ is a function from $\pow{A}$ to $\pow{A}$. + For all $X\in\pow{A}$ we have + $(X,A\setminus \img{g}{B\setminus\img{f}{X}})\in h$ by assumption. + $h$ is a relation by \cref{relation}. + $h$ is right-unique by \cref{rightunique,pair_eq_iff}. + Thus $h$ is a function by assumption. + For all $X\in\pow{A}$ we have + $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ + by \cref{function_apply_intro}. + For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by assumption. + For all $X$ we have if $X\in\dom{h}$, then $X\in\pow{A}$ + by \cref{dom_iff,pair_eq_iff}. + For all $X$ we have if $X\in\pow{A}$, then $X\in\dom{h}$ + by \cref{dom_iff}. + Thus $\dom{h} = \pow{A}$ by set extensionality. + $h$ is a function to $\pow{A}$ by assumption. + Thus $h$ is a function from $\pow{A}$ to $\pow{A}$ by \cref{funs_intro}. $h$ is \subseteq-preserving by \cref{subseteqpreserving,img_subseteq,subseteq_implies_setminus_supseteq}. % apply each each lemma twice (alternating). - Take a fixpoint $X$ of $h$ by \cref{knastertarski}. + Take $X$ such that $X$ is a fixpoint of $h$ by \cref{knastertarski}. Now $X = A\setminus \img{g}{B\setminus\img{f}{X}}$ by \cref{fixpoint}. $\img{g}{B\setminus\img{f}{X}}\subseteq A$. diff --git a/library/status.md b/library/status.md index f5da116..bbb67bd 100644 --- a/library/status.md +++ b/library/status.md @@ -1,8 +1,10 @@ -# Active library migration status +# Active typed library status -This file records the dependency boundary and cutover consequences for the -content-addressed migration. It is not a theorem-authority manifest and does -not duplicate computed IDs or premise lineages. +This file records the active aggregate boundary and the consequences of the +completed content-addressed cutover. It is not a theorem-authority manifest +and does not duplicate computed IDs or premise lineages. Every production +`Verify` invocation uses the exact typed driver; the lists below record the +accepted library inventory, not a routing selector. ## Typed closures @@ -17,7 +19,7 @@ set/suc.tex nat.tex ``` -Phase 5.3 additionally selects these ordinary library roots: +Phase 5.3 activated these ordinary library roots: ```text set/symdiff.tex @@ -32,19 +34,66 @@ relation/uniqueness.tex function.tex set/cantor.tex set/fixpoint.tex +set/equinumerosity.tex +order/quasiorder.tex +order/order.tex +relation/equivalence.tex +relation/closure.tex +algebra/magma.tex +algebra/semigroup.tex +algebra/monoid.tex +algebra/quasigroup.tex +algebra/loop.tex +order/semilattice.tex +topology/preclosure.tex +topology/topological-space.tex +topology/basis.tex +topology/disconnection.tex +topology/separation.tex +ordinal.tex +cardinal.tex +everything.tex ``` -Each selected root has a wholly typed dependency closure. In particular, +Each activated root has a wholly typed dependency closure. In particular, `set/bipartition.tex` imports the typed `set.tex`, `set/cons.tex`, and `set/powerset.tex` modules; `set/product.tex` imports only typed `set.tex`; and `set/filter.tex` imports typed `set.tex` and `set/powerset.tex`. No -selected graph has a legacy edge. The typed `relation.tex` root imports, in +activated graph has an untyped dependency. The typed `relation.tex` root imports, in source order, `set.tex`, `set/powerset.tex`, and `set/product.tex`; its -two selected property modules each import typed `set.tex` and `relation.tex` +two activated property modules each import typed `set.tex` and `relation.tex` in source order. The typed `function.tex` root imports, in source order, -`set.tex`, `relation.tex`, and `relation/uniqueness.tex`. Later relation, -order, and function dependents remain unselected. The typed Cantor and +`set.tex`, `relation.tex`, and `relation/uniqueness.tex`. The typed Cantor and fixpoint roots each import `set/powerset.tex` followed by `function.tex`. +The typed equinumerosity root imports `set/powerset.tex`, `set/fixpoint.tex`, +and `function.tex` in source order. The typed quasiorder root imports +`relation.tex` and `relation/properties.tex`; the typed order root imports +those modules followed by `order/quasiorder.tex`. Both import lists retain +source order. The typed equivalence root imports `set.tex`, +`set/partition.tex`, `relation.tex`, and `order/quasiorder.tex`; the typed +relation-closure root imports `relation/properties.tex` followed by +`relation/equivalence.tex`. The typed magma root imports only `function.tex`, +the semigroup root imports only `algebra/magma.tex`, and the monoid root +imports only `algebra/semigroup.tex`. Quasigroup forms the second branch over +`algebra/magma.tex`; loop imports only `algebra/quasigroup.tex`, whose sealed +interface carries its unital-magma parent as a direct structure parent. These +lists also retain source order. The typed meet-semilattice root imports +`order/order.tex` followed by `function.tex`; the latter is the explicit owner +of source-level graph application used by `meet[X](x,y)`. The standalone typed +preclosure root imports `set.tex` followed by `function.tex` for the same +reason. The typed topological-space root imports `set.tex`, +`set/powerset.tex`, and `set/cons.tex` in source order. The typed basis root +imports `topology/topological-space.tex`, `set.tex`, and `set/powerset.tex`; +the disconnection root imports `set.tex`, `set/bipartition.tex`, and +`topology/topological-space.tex`; and the separation root imports +`topology/topological-space.tex` followed by `set.tex`. These lists retain +source order. The typed ordinal root imports `set.tex`, `set/cons.tex`, +`set/powerset.tex`, `set/regularity.tex`, and `set/suc.tex`; the typed +cardinal root imports `set.tex`, `ordinal.tex`, `function.tex`, and `nat.tex`. +The active `everything.tex` aggregate retains its existing 31 direct +imports in source order. Its complete graph is typed, and it is now the sole +`make lib` corpus root. Other ordinary roots still use the same typed +production driver when invoked directly. ## Fixed-foundation and prelude replacement @@ -87,12 +136,12 @@ the clean checked `PairSetCharacteristic` fact. Tuple notation `(a,b)` resolves to the opaque source-owned ordered-pair object. Its defining and projection axioms retain source-axiom safety. -The production typed-root selection includes the five protected roots and the -twelve Phase 5.3 ordinary library roots. Each selected invocation installs the +The active inventory includes the five protected roots and the twenty-eight +Phase 5.3 ordinary library roots. Every verification invocation acquires the exact packaged final prelude before parsing and uses its syntax and semantics -as the first implicit inputs. The final prelude now supplies `pow_iff` through -the exact clean `PowerSetCharacteristic`; `set/powerset.tex` declares no local -replacement axiom. +as the first implicit inputs. The final prelude supplies +`pow_iff` through the exact clean `PowerSetCharacteristic`; +`set/powerset.tex` declares no local replacement axiom. The base relation module deliberately has mixed, premise-derived authority. Facts whose proofs use only clean set and relation facts, including @@ -122,12 +171,128 @@ definitions have clean defining-equation authority, while Knaster--Tarski inherits `SourceAxiom` safety through the existing function and ordered-pair layer. Neither module introduces a source axiom or an `Omitted` authorization. -`relation/equivalence.tex`, `relation/closure.tex`, all order modules, and -remaining importers of `function.tex`, including `set/equinumerosity.tex`, -remain outside the typed selection. An invocation rooted at one of these -modules therefore remains wholly legacy until its complete graph is migrated. +Equinumerosity is typed against the final prelude and its three sealed direct +imports. Its local function `h` is a scoped replacement graph and its local set +`h'` is likewise proof-local; neither is published in the module interface or +prefix. The ordinary definition has clean defining-equation authority, while +the elementary bijection results inherit the ordered-pair layer's +`SourceAxiom` safety. Cantor--Schroeder--Bernstein retains its single existing +proof-level `Omitted`; the module introduces no source axiom or additional +escape hatch. -The active `library/everything.tex` root remains unselected on the transitional -legacy route and currently does not verify. Its first failure is the removed -`setext` provider referenced by `set.tex`. It must not receive a compatibility -provider or a mixed typed/legacy graph. +The final prelude owns the metadata-only `onesorted structure` descriptor and +its opaque `carrier : Set -> Set` operation. Ordinary structures publish a +transparent predicate definition and independently checked clean projection +facts. `order/quasiorder.tex` owns the opaque `lt` operation; +`order/order.tex` imports that descriptor and reuses the same operation object +without allocating a replacement. Both modules mint neither `SourceAxiom` nor +`Omitted`; ordinary results inherit any ordered-pair safety solely from their +selected premises. + +The equivalence module preserves its transparent quotient and bounded +relation constructions, including source-owned ordered-pair semantics. It +mints no source axiom and retains exactly the five existing direct +`OmittedAuthorization` results at the end of the module. All preceding +declarations check normally. The relation-closure module publishes three +clean transparent defining equations and no direct escape hatch; its +reflexivity theorem truthfully inherits `SourceAxiom` safety through the +selected identity and ordered-pair facts. + +The magma module owns the opaque `mul` operation; unital magma adds the opaque +`neutral` operation. The public `cdot` spelling is a contextual transparent +abbreviation: it keeps surface arity two while its expansion receives the +active structure set as a hidden argument and resolves the exact `mul` object. +The structure definitions and projections are clean, and the module introduces +neither a source axiom nor an `Omitted` authorization. + +The semigroup hierarchy reuses magma's exact `mul` object. Its associativity +and regularity laws quantify over `carrier[A]`; inverse semigroup adds no +operation and proves its inheritance and idempotent-orbit result with ordinary +clean exact authority. It introduces neither a source axiom nor an `Omitted` +authorization. + +Monoid inherits unital magma's exact `mul` and `neutral` objects and restores +the carrier-scoped associativity law. Its implication to semigroup is an +ordinary clean exact proof; the module introduces no operation or escape +hatch. + +Quasigroup inherits magma's `mul` and owns the opaque `ldiv` and `rdiv` +operations in that source order. Its six carrier-scoped laws have stable +projection labels, and both cancellation results are clean exact proofs from +the corresponding division laws. It introduces no escape hatch. + +Loop has direct structure parents quasigroup and unital magma and owns no +operation. The shared `carrier` and `mul` ancestors coalesce by exact object +identity; the descriptor inherits the exact `ldiv`, `rdiv`, and `neutral` +objects without allocating replacements. Its defining and inheritance facts +are clean, and it introduces no escape hatch. + +Meet semilattice has the exact ordered-set parent. Its descriptor reuses the +parent's `carrier` and `lt` objects and owns only the opaque `meet` operation. +Closure, lower-bound, greatest-lower-bound, and idempotence are explicitly +scoped to `carrier[X]`. The structure definition, projections, and theorem +have clean exact authority and introduce no escape hatch. + +Preclosure space has the metadata-only onesorted parent. Its descriptor reuses +the final prelude's exact `carrier` object and owns only the opaque `cl` +operation. Its four labeled laws state carrier-bounded closure, empty-set +preservation, extensivity, and binary-union preservation through explicit +`cl[X]` applications. All generated facts are clean and the module introduces +no theorem, source axiom, or `Omitted` authorization. + +Topological space also has the metadata-only onesorted parent, reuses the exact +`carrier` object, and owns only the opaque `opens` operation. Its four labeled +laws and structure definition are clean. The unqualified `U is open` +abbreviation remains a contextual transparent target requiring that exact +`opens` object; the explicit `U is open in X` form remains available without +an active structure annotation. All ordinary topology definitions are +transparent. The module has no local source axiom and retains exactly its two +pre-existing direct proof omissions, at `interior_elem_elim` and the nested +case in `intersection_of_closed_is_closed_infinite`. Omitted safety propagates +only through selected dependencies; no local fact inherits `SourceAxiom`. + +The three direct topology consumers were activated as sibling maximal roots. +`topology/basis.tex` retains its transparent covering and generated-topology +definitions, and every local fact is clean; explicit local discharges prevent +the imported topology and powerset inventories from contributing incidental +escape safety. `topology/disconnection.tex` retains the opaque source-owned +ordered-pair meaning of `(U,V)`, `fst`, and `snd`. Its reverse theorem and both +definitions are clean, while `disconnection_from_disconnected` truthfully +inherits `SourceAxiom` safety from the selected ordered-pair projection laws. +The module mints no local escape authority. + +`topology/separation.tex` retains exactly six direct proof-level omissions and +mints no source axiom. The two direct omissions in the imported +topological-space interface remain distinct imported authority; no current +ordinary separation fact selects them. Compound separation-space phrases keep +the exact topological-space annotation and therefore reuse the inherited +`carrier` and `opens` objects. Four regularity statements now require the +inhabitedness of `carrier[X]`, rather than incorrectly asserting inhabitedness +of the structure parameter itself; these deliberate statement corrections +change the affected proposition and downstream artifact identities. The +direct omission sites remain scoped to their original theorem candidates. + +The ordinal development introduces no source axiom or omission. Its existing +public definitions and theorem statements retain their mathematical content; +two checked helper lemmas make the nested membership-connex argument explicit +under the exact one-outermost-induction rule. Narrow premise selection keeps +the resulting ordinal facts clean. `cardinal.tex` required no source rewrite: +its transparent finite, infinite, and cardinality declarations compile +directly against the sealed ordinal, function, set, and naturals interfaces. +The aggregate's final reflexive claim has an ordinary checked proof. + +The active aggregate intentionally does not import the typed peripheral +modules `set/equinumerosity.tex` and `topology/preclosure.tex`; they remain +valid typed roots but are not part of the active library inventory. Three +other developments remain outside the active aggregate: `subfinite.tex` +awaits the recorded injection-direction decision, `logic/propositional.tex` +is an experimental standalone +development, and the unused `topology/order-topology.tex` sketch remains +incomplete with duplicate markers and empty laws. If invoked directly, they +still enter the typed driver and receive its ordinary located rejection; no +compatibility provider or fallback exists. + +`make lib` now verifies only `library/everything.tex` against one fresh store. +The aggregate covers every module in its active inventory transitively; +production-corpus verification is no longer repeated across overlapping +frontier roots. diff --git a/library/topology/basis.tex b/library/topology/basis.tex index cc9d7e5..4c1ac79 100644 --- a/library/topology/basis.tex +++ b/library/topology/basis.tex @@ -13,11 +13,23 @@ Suppose $C$ covers $X$. Then $X\subseteq\unions{C}$. \end{proposition} +\begin{proof} + For all $x\in X$ there exists $U\in C$ such that $x\in U$ + by assumption. + For all $x\in X$ we have $x\in\unions{C}$ by \cref{unions_iff}. + Follows by \cref{subseteq}. +\end{proof} \begin{proposition}\label{covers_unions_elim} Suppose $X\subseteq\unions{C}$. Then $C$ covers $X$. \end{proposition} +\begin{proof} + For all $x\in X$ we have $x\in\unions{C}$ by \cref{subseteq}. + For all $x\in X$ there exists $U\in C$ such that $x\in U$ + by \cref{unions_iff}. + Follows by assumption. +\end{proof} % Also called "prebase", "subbasis", or "subbase". We prefer "pre-" or "quasi-" % for consistency when handling generalizations, even if "subbasis" is more common. @@ -36,6 +48,7 @@ If $\unions{B} = X$, then $B$ is a family of subsets of $X$ and $B$ covers $X$ by \cref{covers_unions_intro,subseteq_refl,covers_unions_elim}. + Follows by assumption. \end{proof} % Also called "base of topology". @@ -55,6 +68,13 @@ Assume $B$ is a topological basis for $X$. $\emptyset \in \genOpens{B}{X}$. \end{lemma} +\begin{proof} + $\emptyset\in\pow{X}$ by \cref{emptyset_subseteq,pow_iff}. + For all $x\in\emptyset$ there exists $V\in B$ + such that $x\in V\subseteq\emptyset$ + by \cref{emptyset_subseteq,subseteq}. + Follows by \cref{genopens}. +\end{proof} @@ -64,18 +84,25 @@ Then $\unions{F}\in\genOpens{B}{X}$. \end{lemma} \begin{proof} - We have $\unions{F} \in \pow{X}$ by \cref{genopens,subseteq,pow_iff,unions_family,powerset_elim}. + For all $x\in\unions{F}$ we have $x\in X$ + by \cref{unions_iff,genopens,subseteq}. + We have $\unions{F}\in\pow{X}$ by \cref{pow_iff,subseteq}. - Show for all $x\in \unions{F}$ there exists $W \in B$ - such that $x\in W$ and $W \subseteq \unions{F}$. + Show for all $x$ we have if $x\in\unions{F}$, then + there exists $W\in B$ such that $x\in W$ and + $W\subseteq\unions{F}$. \begin{subproof} - Fix $x \in \unions{F}$. - There exists $V \in F$ such that $x \in V$ by \cref{unions_iff}. - $V \in \genOpens{B}{X}$. - There exists $W \in B$ such that $x \in W \subseteq V$. - Then $W \subseteq \unions{F}$. + Fix $x$. + Assume $x\in\unions{F}$. + Take $V$ such that $V\in F$ and $x\in V$ by \cref{unions_iff}. + $V\in\genOpens{B}{X}$ by \cref{subseteq}. + Take $W$ such that $W\in B$ and $x\in W\subseteq V$ + by \cref{genopens}. + $V\subseteq\unions{F}$ by \cref{unions_iff,subseteq}. + $W\subseteq\unions{F}$ by \cref{subseteq_transitive}. + Follows by assumption. \end{subproof} - Then $\unions{F}\in\genOpens{B}{X}$ by \cref{genopens}. + Follows by \cref{genopens}. \end{proof} \begin{lemma}\label{basis_is_in_genopens} @@ -83,14 +110,19 @@ $B \subseteq \genOpens{B}{X}$. \end{lemma} \begin{proof} - We show for all $V \in B$ $V \in \genOpens{B}{X}$. + Show for all $V$ we have if $V\in B$, then + $V\in\genOpens{B}{X}$. \begin{subproof} - Fix $V \in B$. - For all $x \in V$ $x \in V \subseteq V$. - $V \subseteq X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. - $V \in \pow{X}$. - $V \in \genOpens{B}{X}$. + Fix $V$. + Assume $V\in B$. + $V\subseteq X$ + by \cref{topological_prebasis_iff_covering_family,topological_basis}. + $V\in\pow{X}$ by \cref{pow_iff,subseteq}. + For all $x\in V$ there exists $W\in B$ + such that $x\in W\subseteq V$ by \cref{subseteq_refl}. + Follows by \cref{genopens}. \end{subproof} + Follows by \cref{subseteq}. \end{proof} \begin{lemma}\label{all_is_in_genopens} @@ -98,11 +130,10 @@ $X \in \genOpens{B}{X}$. \end{lemma} \begin{proof} - $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. - $\unions{B} \in \genOpens{B}{X}$. - $X \subseteq \unions{B}$. - For all $x\in X$ there exists $V\in B$ such that $x\in V\subseteq X$. - Follows by \cref{powerset_top,genopens}. + $X\in\pow{X}$ by \cref{pow_iff,subseteq_refl}. + For all $x\in X$ there exists $V\in B$ such that $x\in V\subseteq X$ + by \cref{topological_prebasis_iff_covering_family,topological_basis,pow_iff,subseteq}. + Follows by \cref{genopens}. \end{proof} \begin{lemma}\label{inters_in_genopens} @@ -111,23 +142,25 @@ Then $(A\inter C) \in \genOpens{B}{X}$. \end{lemma} \begin{proof} + For all $x\in A\inter C$ we have $x\in X$ + by \cref{genopens,inter_elim_left,pow_iff,subseteq}. + We have $(A\inter C)\in\pow{X}$ by \cref{pow_iff,subseteq}. - We have $(A \inter C) \in \pow{X}$ by \cref{genopens,inter_powerset}. - - Show for all $x\in A\inter C$ there exists $W \in B$ - such that $x\in W$ and $W \subseteq A\inter C$. + Show for all $x$ we have if $x\in A\inter C$, then + there exists $W\in B$ such that $x\in W$ and $W\subseteq A\inter C$. \begin{subproof} - Fix $x \in A\inter C$. - Then $x\in A,C$. - There exists $V' \in B$ such that $x \in V' \subseteq A$ by \cref{genopens}. - There exists $V'' \in B$ such that $x \in V''\subseteq C$ by \cref{genopens}. - There exists $W \in B$ such that $x \in W \subseteq V', V''$ by \cref{topological_basis}. - - Show $W \subseteq A\inter C$. - \begin{subproof} - For all $y \in W$ we have $y \in V'$ and $y \in V''$. - \end{subproof} + Fix $x$. + Assume $x\in A\inter C$. + $x\in A,C$ by \cref{inter_elim_left,inter_elim_right}. + Take $V'$ such that $V'\in B$ and $x\in V'\subseteq A$ + by \cref{genopens}. + Take $V''$ such that $V''\in B$ and $x\in V''\subseteq C$ + by \cref{genopens}. + Take $W$ such that $W\in B$ and $x\in W$ and + $W\subseteq V',V''$ by \cref{topological_basis}. + $W\subseteq A,C$ by \cref{subseteq_transitive}. + $W\subseteq A\inter C$ by \cref{inter_intro,subseteq}. + Follows by assumption. \end{subproof} - - $(A\inter C) \in \genOpens{B}{X}$ by \cref{genopens}. + Follows by \cref{genopens}. \end{proof} diff --git a/library/topology/disconnection.tex b/library/topology/disconnection.tex index e3730f3..90c635d 100644 --- a/library/topology/disconnection.tex +++ b/library/topology/disconnection.tex @@ -23,10 +23,14 @@ Then there exists a disconnection of $X$. \end{proposition} \begin{proof} - Take $U, V\in\opens[X]$ such that $\carrier[X]$ is partitioned by $U$ and $V$ + Take $U,V$ such that $U,V\in\opens[X]$ and + $\carrier[X]$ is partitioned by $U$ and $V$ by \cref{disconnected}. - Then $(U, V)$ is a bipartition of $\carrier[X]$. - Thus $(U, V)$ is a disconnection of $X$ by \cref{disconnections,times_proj_elim,times_tuple_intro}. + $(U,V)$ is a bipartition of $\carrier[X]$ by \cref{bipartition_intro}. + $\fst{(U,V)}=U$ by \cref{fst_eq}. + $\snd{(U,V)}=V$ by \cref{snd_eq}. + $(U,V)\in\disconnections{X}$ by \cref{disconnections}. + Follows by assumption. \end{proof} \begin{proposition}\label{disconnected_from_disconnection} @@ -35,8 +39,12 @@ Then $X$ is disconnected. \end{proposition} \begin{proof} - $\fst{D}, \snd{D}\in\opens[X]$. - $\carrier[X]$ is partitioned by $\fst{D}$ and $\snd{D}$. + $D\in\disconnections{X}$ by assumption. + $D\in\bipartitions{\carrier[X]}$ by \cref{disconnections}. + $\fst{D},\snd{D}\in\opens[X]$ by \cref{disconnections}. + $\carrier[X]$ is partitioned by $\fst{D}$ and $\snd{D}$ + by \cref{bipartitions_of_a_set}. + Follows by \cref{disconnected}. \end{proof} \begin{abbreviation}\label{connected} diff --git a/library/topology/preclosure.tex b/library/topology/preclosure.tex index 6c104be..e9ed27f 100644 --- a/library/topology/preclosure.tex +++ b/library/topology/preclosure.tex @@ -1,18 +1,22 @@ \import{set.tex} +\import{function.tex} \section{Preclosure spaces} -\begin{struct} +\begin{struct}\label{preclosure_space} A preclosure space $X$ is a onesorted structure equipped with \begin{enumerate} \item $\cl$ \end{enumerate} such that \begin{enumerate} - \item For all $Y\subseteq X$ we have $\cl(Y)\subseteq X$. - \item $\cl(\emptyset) = \emptyset$. - \item For all $A$ we have $A\subseteq \cl(A)$. - \item For all $A, B$ we have $\cl(A\union B) = \cl(A) \union \cl(B)$. + \item\label{preclosure_type} For all $Y\subseteq\carrier[X]$ we have + $\cl[X](Y)\subseteq\carrier[X]$. + \item\label{preclosure_empty} $\cl[X](\emptyset)=\emptyset$. + \item\label{preclosure_extensive} For all $A\subseteq\carrier[X]$ we have + $A\subseteq\cl[X](A)$. + \item\label{preclosure_union} For all $A,B\subseteq\carrier[X]$ we have + $\cl[X](A\union B)=\cl[X](A)\union\cl[X](B)$. \end{enumerate} \end{struct} diff --git a/library/topology/separation.tex b/library/topology/separation.tex index ad8cad1..5806216 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -32,11 +32,13 @@ $x\in A\not\ni y$ or $x\notin A\ni y$. \end{proposition} \begin{proof} - Take $U\in\opens[X]$ such that $x\in U\not\ni y$ or $x\notin U\ni y$ + Take $U$ such that + $U\in\opens[X]\land ((x\in U\land y\notin U)\lor(x\notin U\land y\in U))$ by \cref{is_kolmogorov}. Then $\carrier[X]\setminus U\in\closeds{X}$ by \cref{complement_of_open_elem_closeds}. Now $x\in (\carrier[X]\setminus U)\not\ni y$ or $x\notin (\carrier[X]\setminus U)\ni y$ by \cref{setminus}. + Follows by assumption. \end{proof} \begin{proposition}\label{kolmogorov_for_closeds_implies_kolmogorov} @@ -138,15 +140,7 @@ Then $X$ is a \teeone-space. \end{proposition} \begin{proof} - We show that for all $x,y\in\carrier[X]$ such that $x\neq y$ - there exist $U, V\in\opens[X]$ such that - $U\ni x\notin V$ and $V\ni y\notin U$. - \begin{subproof} - $X$ is hausdorff. - For all $x,y\in\carrier[X]$ such that $x\neq y$ - there exist $U, V\in\opens[X]$ such that - $x\in U$ and $y\in V$ and $U$ is disjoint from $V$. - \end{subproof} + Follows by \cref{is_hausdorff,teeone,disjoint}. \end{proof} \begin{definition}\label{is_regular} @@ -168,7 +162,7 @@ \begin{proposition}\label{teethree_implies_closed_neighbourhood_in_open} Let $X$ be a topological space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. Suppose $X$ is \teethree\ . For all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. \end{proposition} @@ -193,7 +187,7 @@ \begin{proposition}\label{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods} Let $X$ be a topological space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. $X$ is \teethree\ iff for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$. \end{proposition} \begin{proof} @@ -207,12 +201,13 @@ \begin{subproof} Omitted. \end{subproof} + Follows by assumption. \end{proof} \begin{proposition}\label{teethree_iff_closed_neighbourhood_in_open} Let $X$ be a topological space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. $X$ is \teethree\ iff for all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. \end{proposition} \begin{proof} @@ -223,7 +218,7 @@ \begin{proposition}\label{teethree_space_is_teetwo_space} Let $X$ be a \teethree-space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. Then $X$ is a \teetwo-space. \end{proposition} \begin{proof} diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index 8076c5f..4f3eb38 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -41,9 +41,10 @@ Then $A\union B$ is open. \end{proposition} \begin{proof} - $\{A, B\}\subseteq \opens$. - $\unions{\{A, B\}}$ is open. - $\unions{\{A, B\}} = A\union B$. + $\{A, B\}\subseteq\opens$ by \cref{cons_iff,subseteq}. + $\unions{\{A, B\}}$ is open by \cref{opens_unions}. + $\unions{\{A, B\}}=A\union B$ by \cref{union_as_unions}. + Follows by assumption. \end{proof} \begin{definition}[Interiors]\label{interiors} @@ -59,7 +60,8 @@ Then $a\in\interior{A}{X}$. \end{proposition} \begin{proof} - $U\in\interiors{A}{X}$. + $U\in\interiors{A}{X}$ by \cref{interiors}. + Follows by \cref{interior,unions_intro}. \end{proof} \begin{proposition}[Interior]\label{interior_elem_elim} @@ -87,7 +89,7 @@ Then $\interior{U}{X} = U$. \end{proposition} \begin{proof} - $U\in\interiors{U}{X}$. + $U\in\interiors{U}{X}$ by \cref{interiors,subseteq_refl}. Follows by \cref{subseteq,interior_elem_iff,neq_witness}. \end{proof} @@ -96,12 +98,18 @@ Then $\interior{A}{X}$ is open. \end{proposition} \begin{proof} - $\interiors{A}{X}\subseteq\opens[X]$. + $\interiors{A}{X}\subseteq\opens[X]$ by \cref{interiors,subseteq}. + Follows by \cref{interior,opens_unions}. \end{proof} \begin{proposition}\label{interior_subseteq} Then $\interior{A}{X}\subseteq A$. \end{proposition} +\begin{proof} + For all $U\in\interiors{A}{X}$ we have $U\subseteq A$ + by \cref{interiors}. + Follows by \cref{interior,unions_iff,subseteq}. +\end{proof} \begin{proposition}\label{interior_maximal} Let $X$ be a topological space. @@ -109,27 +117,36 @@ Suppose $U$ is open. Then $U\subseteq \interior{A}{X}$. \end{proposition} +\begin{proof} + $U\in\interiors{A}{X}$ by \cref{interiors}. + $U\subseteq\unions{\interiors{A}{X}}$ by \cref{unions_iff,subseteq}. + Follows by \cref{interior}. +\end{proof} \begin{proposition}\label{interior_eq_self_implies_open} Let $X$ be a topological space. Suppose $\interior{A}{X} = A$. Then $A$ is open. \end{proposition} +\begin{proof} + $\interior{A}{X}$ is open by \cref{interior_is_open}. + Follows by assumption. +\end{proof} \begin{corollary}\label{interior_eq_self_iff_open} Let $X$ be a topological space. Then $\interior{A}{X} = A$ iff $A$ is open in $X$. \end{corollary} +\begin{proof} + Follows by \cref{interior_eq_self_implies_open,interior_of_open}. +\end{proof} \begin{proposition}\label{interior_carrier} Let $X$ be a topological space. $\interior{\carrier[X]}{X} = \carrier[X]$. \end{proposition} \begin{proof} - $\carrier[X]\in\opens[X]$. - $\carrier[X]\subseteq\carrier[X]$ by \cref{subseteq_refl}. - Thus $\carrier[X]\in\interiors{\carrier[X]}{X}$ by \cref{interiors}. - Follows by set extensionality. + Follows by \cref{carrier_open,interior_of_open}. \end{proof} \begin{proposition}\label{interior_type} @@ -137,10 +154,11 @@ Then $\interior{A}{X}\in\pow{\carrier[X]}$. \end{proposition} \begin{proof} - We have $\interiors{A}{X}\subseteq \pow{\carrier[X]}$. - % As they are open subsets of X containing A - % - Thus $\interior{A}{X}\subseteq \carrier[X]$ by \cref{interior,unions_subseteq_of_powerset_is_subseteq}. + We have $\interiors{A}{X}\subseteq \pow{\carrier[X]}$ + by \cref{interiors,opens_type,subseteq}. + For all $x\in\interior{A}{X}$ we have $x\in\carrier[X]$ + by \cref{interior,unions_iff,pow_iff,subseteq}. + Follows by \cref{pow_iff}. \end{proof} \subsection{Closed sets} @@ -158,7 +176,8 @@ Then $\emptyset$ is closed in $X$. \end{proposition} \begin{proof} - $\carrier[X]\setminus \emptyset = \carrier[X]$. + $\carrier[X]\setminus \emptyset = \carrier[X]$ by \cref{setminus_emptyset}. + Follows by \cref{is_closed_in,carrier_open}. \end{proof} \begin{proposition}\label{carrier_is_closed} @@ -166,7 +185,7 @@ Then $\carrier[X]$ is closed in $X$. \end{proposition} \begin{proof} - $\carrier[X]\setminus \carrier[X] = \emptyset$. + $\carrier[X]\setminus \carrier[X] = \emptyset$ by \cref{setminus_self}. Follows by \cref{emptyset_open,is_closed_in}. \end{proof} @@ -191,10 +210,14 @@ Then $\carrier[X]\setminus U\in\closeds{X}$. \end{proposition} \begin{proof} - $\carrier[X]\setminus U\in\pow{\carrier[X]}$. + $\carrier[X]\setminus U\subseteq\carrier[X]$ + by \cref{setminus_subseteq}. + $\carrier[X]\setminus U\in\pow{\carrier[X]}$ + by \cref{pow_iff,subseteq}. $U\subseteq\carrier[X]$ by \cref{opens_type}. Hence $\carrier[X]\setminus(\carrier[X]\setminus U) = U$ by \cref{double_relative_complement}. - $\carrier[X]\setminus U$ is closed in $X$. + $\carrier[X]\setminus U$ is closed in $X$ by \cref{is_closed_in}. + Follows by \cref{closeds}. \end{proof} @@ -211,7 +234,14 @@ Then $\closure{\emptyset}{X} = \emptyset$. \end{proposition} \begin{proof} - $\emptyset\in\closures{\emptyset}{X}$. + $\emptyset\in\pow{\carrier[X]}$ by \cref{emptyset_subseteq,pow_iff}. + $\emptyset$ is closed in $X$ by \cref{emptyset_is_closed}. + $\emptyset\in\closures{\emptyset}{X}$ by \cref{closures,subseteq_refl}. + For all $x\in\closure{\emptyset}{X}$ we have $x\in\emptyset$ + by \cref{closure,inters_subseteq_elem,subseteq}. + For all $x\in\emptyset$ we have $x\in\closure{\emptyset}{X}$ + by \cref{emptyset_subseteq,subseteq}. + Follows by set extensionality. \end{proof} \begin{proposition}\label{closure_carrier} @@ -219,12 +249,18 @@ Then $\closure{\carrier[X]}{X} = \carrier[X]$. \end{proposition} \begin{proof} - %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\subseteq D$ by \cref{closures}. - %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\supseteq D$ by \cref{pow_iff,closures}. - %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X] = D$ by \cref{subseteq_antisymmetric}. + For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\subseteq D$ + by \cref{closures}. + For all $D\in\closures{\carrier[X]}{X}$ we have + $D\in\pow{\carrier[X]}$ by \cref{closures}. + For all $D\in\closures{\carrier[X]}{X}$ we have $D\subseteq\carrier[X]$ + by \cref{pow_iff,subseteq}. For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X] = D$ - by \cref{pow_iff,closures,subseteq_antisymmetric}. - Now $\carrier[X]\in\closures{\carrier[X]}{X}$. + by \cref{subseteq_antisymmetric}. + $\carrier[X]\subseteq\carrier[X]$ by \cref{subseteq_refl}. + $\carrier[X]\in\pow{\carrier[X]}$ by \cref{pow_iff,subseteq}. + Now $\carrier[X]\in\closures{\carrier[X]}{X}$ + by \cref{closures,carrier_is_closed}. Thus $\closures{\carrier[X]}{X} = \{\carrier[X]\}$ by \cref{singleton_iff_inhabited_subsingleton}. Follows by \cref{inters_singleton,closure}. @@ -235,6 +271,9 @@ Suppose $A \subseteq \inters{F}$. Then for all $X \in F$ we have $A \subseteq X$. \end{proposition} +\begin{proof} + Follows by \cref{inters_subseteq_elem,subseteq}. +\end{proof} \begin{proposition}\label{subseteq_of_all_then_subset_of_union} @@ -244,8 +283,10 @@ Then $A \subseteq \unions{F}$. \end{proposition} \begin{proof} - There exist $X \in F$ such that $X \subseteq \unions{F}$. - $A \subseteq X \subseteq \unions{F}$. + Take $X$ such that $X\in F$ by assumption. + $X\subseteq\unions{F}$ by \cref{unions_iff,subseteq}. + $A\subseteq X$ by assumption. + Follows by \cref{subseteq_transitive}. \end{proof} @@ -257,22 +298,20 @@ Then $A \subseteq \inters{F}$. \end{proposition} \begin{proof} - \begin{byCase} - \caseOf{$A = \emptyset$.}Trivial. - \caseOf{$A \neq \emptyset$.} - $F$ is inhabited. - It suffices to show that for all $a \in A$ we have $a \in \inters{F}$. - Fix $a \in A$. - For all $X \in F$ we have $a \in X$. - $A \subseteq \unions{F}$. - $a \in \unions{F}$. - \end{byCase} + For all $a\in A$ we have for all $X\in F$ we have $a\in X$ + by \cref{subseteq}. + For all $a\in A$ we have $a\in\inters{F}$ + by \cref{inters_iff_forall}. + Follows by \cref{subseteq}. \end{proof} \begin{proposition}\label{subseteq_inters_iff_new} Suppose $F$ is inhabited. $A \subseteq \inters{F}$ iff for all $X \in F$ we have $A \subseteq X$. \end{proposition} +\begin{proof} + Follows by \cref{subseteq_inters_iff_to_left,subseteq_inters_iff_to_right}. +\end{proof} \begin{proposition}\label{set_is_subseteq_to_closure_of_the_set} Let $X$ be a topological space. @@ -280,19 +319,16 @@ $A \subseteq \closure{A}{X}$. \end{proposition} \begin{proof} - \begin{byCase} - \caseOf{$A = \emptyset$.} - Trivial. - \caseOf{$A \neq \emptyset$.} - We show that $\carrier[X] \in \closures{A}{X}$. - \begin{subproof} - $\carrier[X]$ is closed in $X$. - $\carrier[X] \in \pow{\carrier[X]}$. - \end{subproof} - $\closures{A}{X}$ is inhabited. - For all $A' \in \closures{A}{X}$ we have $A \subseteq A'$. - Therefore $A \subseteq \inters{\closures{A}{X}}$ by \cref{subseteq_inters_iff}. - \end{byCase} + $\carrier[X]\in\pow{\carrier[X]}$ by \cref{pow_iff,subseteq_refl}. + $\carrier[X]$ is closed in $X$ by \cref{carrier_is_closed}. + $\carrier[X]\in\closures{A}{X}$ + by \cref{closures,subseteq_refl}. + $\closures{A}{X}$ is inhabited by assumption. + For all $A'\in\closures{A}{X}$ we have $A\subseteq A'$ + by \cref{closures}. + $A\subseteq\inters{\closures{A}{X}}$ + by \cref{subseteq_inters_iff_to_left}. + Follows by \cref{closure}. \end{proof} \begin{proposition}\label{complement_of_closure_of_complement_of_x_subseteq_x} @@ -301,10 +337,20 @@ $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$. \end{proposition} \begin{proof} - It suffices to show that for all $x \in (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$ we have $x \in A$. - Fix $x$. - If $x \in \carrier[X]\setminus A$ then $x \in \closure{(\carrier[X]\setminus A)}{X}$ by \cref{set_is_subseteq_to_closure_of_the_set,setminus_subseteq,elem_subseteq,setminus}. - Follows by \cref{subseteq_setminus_cons_elim,cons_absorb,double_complement_union,union_as_unions,set_is_subseteq_to_closure_of_the_set,setminus_subseteq,setminus_intro,closure,setminus_elim_left}. + For all $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ + we have $x\in\carrier[X]$ + by \cref{setminus_elim_left}. + For all $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ + we have $x\notin\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{setminus_elim_right}. + For all $x$ we have if + $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ and + $x\in\carrier[X]\setminus A$, then + $x\in\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{set_is_subseteq_to_closure_of_the_set,setminus_subseteq,subseteq}. + For all $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ + we have $x\in A$ by \cref{setminus}. + Follows by \cref{subseteq}. \end{proof} \begin{proposition}\label{complement_of_closed_is_open} @@ -313,6 +359,9 @@ Suppose $A$ is closed in $X$. Then $\carrier[X] \setminus A$ is open in $X$. \end{proposition} +\begin{proof} + Follows by \cref{is_closed_in}. +\end{proof} \begin{proposition}\label{complement_of_open_is_closed} Let $X$ be a topological space. @@ -320,31 +369,46 @@ Suppose $A$ is open in $X$. Then $\carrier[X] \setminus A$ is closed in $X$. \end{proposition} +\begin{proof} + $\carrier[X]\setminus(\carrier[X]\setminus A)=A$ + by \cref{double_relative_complement}. + Follows by \cref{is_closed_in}. +\end{proof} \begin{proposition}\label{intersection_of_closed_is_closed} Let $X$ be a topological space. Suppose $A, B \subseteq \carrier[X]$. - Suppose $A$ are closed in $X$. - Suppose $B$ are closed in $X$. + Suppose $A$ is closed in $X$. + Suppose $B$ is closed in $X$. Then $A \inter B$ is closed in $X$. \end{proposition} \begin{proof} - $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$. - $(\carrier[X] \setminus A) \union (\carrier[X] \setminus B) \in \opens[X]$. - $A \inter B = \carrier[X] \setminus ((\carrier[X] \setminus A) \union (\carrier[X] \setminus B))$. + $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$ + by \cref{is_closed_in}. + $(\carrier[X] \setminus A) \union (\carrier[X] \setminus B) + \in \opens[X]$ by \cref{union_open}. + $\carrier[X]\setminus(A\inter B) + =(\carrier[X]\setminus A)\union(\carrier[X]\setminus B)$ + by \cref{setminus_inter}. + Follows by \cref{is_closed_in}. \end{proof} \begin{proposition}\label{union_of_closed_is_closed} Let $X$ be a topological space. Suppose $A, B \subseteq \carrier[X]$. - Suppose $A$ are closed in $X$. - Suppose $B$ are closed in $X$. + Suppose $A$ is closed in $X$. + Suppose $B$ is closed in $X$. Then $A \union B$ is closed in $X$. \end{proposition} \begin{proof} - $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$. - $(\carrier[X] \setminus A) \inter (\carrier[X] \setminus B) \in \opens[X]$. - $A \union B = \carrier[X] \setminus ((\carrier[X] \setminus A) \inter (\carrier[X] \setminus B))$. + $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$ + by \cref{is_closed_in}. + $(\carrier[X] \setminus A) \inter (\carrier[X] \setminus B) + \in \opens[X]$ by \cref{opens_inter}. + $\carrier[X]\setminus(A\union B) + =(\carrier[X]\setminus A)\inter(\carrier[X]\setminus B)$ + by \cref{setminus_union}. + Follows by \cref{is_closed_in}. \end{proof} \begin{proposition}\label{closed_minus_open_is_closed} @@ -354,6 +418,15 @@ Suppose $B$ is closed in $X$. Then $B \setminus A$ is closed in $X$. \end{proposition} +\begin{proof} + $\carrier[X]\setminus A\subseteq\carrier[X]$ + by \cref{setminus_subseteq}. + $\carrier[X]\setminus A$ is closed in $X$ + by \cref{complement_of_open_is_closed}. + $B\inter(\carrier[X]\setminus A)$ is closed in $X$ + by \cref{intersection_of_closed_is_closed}. + Follows by \cref{setminus_eq_inter_complement}. +\end{proof} @@ -366,42 +439,45 @@ \end{proposition} \begin{proof} Let $F' = \{Y \in \pow{\carrier[X]} \mid \text{there exists $C \in F$ such that $Y = \carrier[X] \setminus C$ }\} $. - For all $Y \in F'$ we have $Y$ is open in $X$. - $\unions{F'}$ is open in $X$. - $\unions{F'}, \inters{F} \subseteq \carrier[X]$. - We show that $\inters{F} = \carrier[X] \setminus (\unions{F'})$. + Show for all $Y$ we have if $Y\in F'$, then $Y$ is open in $X$. + \begin{subproof} + Fix $Y$. + Assume $Y\in F'$. + Take $C$ such that $C\in F$ and + $Y=\carrier[X]\setminus C$ by assumption. + $C$ is closed in $X$ by assumption. + $\carrier[X]\setminus C$ is open in $X$ + by \cref{complement_of_closed_is_open,pow_iff,subseteq}. + Follows by assumption. + \end{subproof} + $F'\subseteq\opens[X]$ by \cref{subseteq}. + $\unions{F'}$ is open in $X$ by \cref{opens_unions}. + $\unions{F'}\subseteq\carrier[X]$ + by \cref{opens_type,unions_iff,pow_iff,subseteq}. + $\inters{F}\subseteq\carrier[X]$ + by \cref{inters_iff_forall,pow_iff,subseteq}. + Show $\inters{F} = \carrier[X] \setminus (\unions{F'})$. \begin{subproof} - We show that for all $a \in \inters{F}$ we have $a \in \carrier[X] \setminus (\unions{F'})$. + Show for all $a$ we have if $a\in\inters{F}$, then + $a\in\carrier[X]\setminus\unions{F'}$. \begin{subproof} - Fix $a \in \inters{F}$. - $a \in \carrier[X]$. - For all $A \in F$ we have $a \in A$. - For all $A \in F$ we have $a \notin (\carrier[X] \setminus A)$. - Then $a \notin \unions{F'}$. - Therefore $a \in \carrier[X] \setminus (\unions{F'})$. + Fix $a$. + Assume $a\in\inters{F}$. + $a\in\carrier[X]$ + by \cref{inters_iff_forall,pow_iff,subseteq}. + For all $A\in F$ we have $a\in A$ + by \cref{inters_iff_forall}. + For all $A\in F$ we have + $a\notin\carrier[X]\setminus A$ by \cref{setminus}. + $a\notin\unions{F'}$ by \cref{unions_iff}. + Follows by \cref{setminus_intro}. \end{subproof} - We show that for all $a \in \carrier[X] \setminus (\unions{F'})$ we have $a \in \inters{F}$. + Show for all $a$ we have if + $a\in\carrier[X]\setminus\unions{F'}$, then $a\in\inters{F}$. \begin{subproof} - \begin{byCase} - \caseOf{$\inters{F} = \emptyset$.} - $F$ is inhabited. - Take $U$ such that $U \in F$. - Let $F'' = F \setminus \{U\}$. - There exist $U' \in F'$ such that $U' = \carrier[X] \setminus U$. - Omitted. - \caseOf{$\inters{F} \neq \emptyset$.} - - Fix $a \in \carrier[X] \setminus (\unions{F'})$. - $\inters{F}$ is inhabited. - $a \in \carrier[X]$. - $a \notin \unions{F'}$. - For all $A \in F'$ we have $a \notin A$. - For all $A \in F'$ we have $a \in (\carrier[X] \setminus A)$. - For all $A \in F'$ there exists $Y \in F$ such that $Y = (\carrier[X] \setminus A)$ by \cref{setminus_setminus,inter_absorb_supseteq_left,pow_iff,subseteq}. - For all $Y \in F $ there exists $A \in F'$ such that $a \in Y = (\carrier[X] \setminus A)$. - For all $Y \in F$ we have $a \in Y$. - Therefore $a \in \inters{F}$. - \end{byCase} + Fix $a$. + Assume $a\in\carrier[X]\setminus\unions{F'}$. + Omitted. \end{subproof} Follows by set extensionality. \end{subproof} @@ -414,15 +490,15 @@ Then $\closure{A}{X}$ is closed in $X$. \end{proposition} \begin{proof} - \begin{byCase} - \caseOf{$\closure{A}{X} = \emptyset$.} - Trivial. - \caseOf{$\closure{A}{X} \neq \emptyset$.} - $\closures{A}{X}$ is inhabited. - $\closures{A}{X} \subseteq \pow{\carrier[X]}$. - For all $B \in \closures{A}{X}$ we have $B$ is closed in $X$. - $\inters{\closures{A}{X}}$ is closed in $X$. - \end{byCase} + $\carrier[X]\in\closures{A}{X}$ + by \cref{closures,pow_iff,carrier_is_closed,subseteq_refl}. + $\closures{A}{X}$ is inhabited by assumption. + $\closures{A}{X}\subseteq\pow{\carrier[X]}$ by \cref{closures,subseteq}. + For all $B\in\closures{A}{X}$ we have $B$ is closed in $X$ + by \cref{closures}. + $\inters{\closures{A}{X}}$ is closed in $X$ + by \cref{intersection_of_closed_is_closed_infinite}. + Follows by \cref{closure}. \end{proof} @@ -441,6 +517,9 @@ Suppose $A \subseteq \carrier[X]$. For all $Y \in \opens[X]$ such that $Y \subseteq A$ we have $Y \subseteq \interior{A}{X}$. \end{proposition} +\begin{proof} + Follows by \cref{interior_maximal}. +\end{proof} \begin{proposition}\label{complement_interior_eq_closure_complement} Let $X$ be a topological space. @@ -448,22 +527,39 @@ $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$. \end{proposition} \begin{proof} - We show that for all $x \in \carrier[X]\setminus\interior{A}{X}$ we have $x \in \closure{(\carrier[X]\setminus A)}{X}$. - \begin{subproof} - Fix $x \in \carrier[X]\setminus\interior{A}{X}$. - Suppose not. - $x \notin \closure{(\carrier[X]\setminus A)}{X}$. - $x \in \carrier[X]$. - $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \inter \closure{(\carrier[X]\setminus A)}{X} = \emptyset$. - $x \in A$. - $x \in A \inter (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$. - $\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X} \in \opens[X]$. - There exist $U \in \opens[X]$ such that $x \in U$ and $U\subseteq A$. - $U \subseteq \interior{A}{X}$. - Contradiction. - \end{subproof} - $\carrier[X]\setminus\interior{A}{X} \subseteq \closure{(\carrier[X]\setminus A)}{X}$. - $\closure{(\carrier[X]\setminus A)}{X} \subseteq \carrier[X]\setminus\interior{A}{X}$. % SLOW by \cref{setminus_subseteq,interior_is_open,complement_of_open_elem_closeds,subseteq_implies_setminus_supseteq,closure_is_minimal_closed_set}. + $\carrier[X]\setminus A\subseteq\carrier[X]$ by \cref{setminus_subseteq}. + $\carrier[X]\in\closeds{X}$ + by \cref{closeds,pow_iff,carrier_is_closed,subseteq_refl}. + $\closure{(\carrier[X]\setminus A)}{X}\subseteq\carrier[X]$ + by \cref{closure_is_minimal_closed_set}. + $\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ + is open in $X$ by \cref{closure_is_closed,complement_of_closed_is_open}. + $\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}\subseteq A$ + by \cref{complement_of_closure_of_complement_of_x_subseteq_x}. + $\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X} + \subseteq\interior{A}{X}$ by \cref{interior_maximal}. + $\carrier[X]\setminus\interior{A}{X} + \subseteq\carrier[X]\setminus + (\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X})$ + by \cref{subseteq_implies_setminus_supseteq}. + $\carrier[X]\setminus + (\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}) + =\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{double_relative_complement}. + $\carrier[X]\setminus\interior{A}{X} + \subseteq\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{subseteq_transitive}. + + $\interior{A}{X}\subseteq A$ by \cref{interior_subseteq}. + $\carrier[X]\setminus A + \subseteq\carrier[X]\setminus\interior{A}{X}$ + by \cref{subseteq_implies_setminus_supseteq}. + $\carrier[X]\setminus\interior{A}{X}\in\closeds{X}$ + by \cref{interior_is_open,complement_of_open_elem_closeds}. + $\closure{(\carrier[X]\setminus A)}{X} + \subseteq\carrier[X]\setminus\interior{A}{X}$ + by \cref{closure_is_minimal_closed_set}. + Follows by \cref{subseteq_antisymmetric}. \end{proof} @@ -477,6 +573,17 @@ Suppose $A \subseteq \carrier[X]$. Then $\closure{A}{X}, \interior{A}{X}, \frontier{A}{X} \subseteq \carrier[X]$. \end{proposition} +\begin{proof} + $\carrier[X]\in\closeds{X}$ + by \cref{closeds,pow_iff,carrier_is_closed,subseteq_refl}. + $\closure{A}{X}\subseteq\carrier[X]$ + by \cref{closure_is_minimal_closed_set}. + $\interior{A}{X}\subseteq\carrier[X]$ + by \cref{interior_type,pow_iff,subseteq}. + $\frontier{A}{X}\subseteq\carrier[X]$ + by \cref{frontier,setminus_subseteq,subseteq_transitive}. + Follows by assumption. +\end{proof} \begin{proposition}\label{frontier_is_closed} Let $X$ be a topological space. @@ -484,13 +591,22 @@ Then $\frontier{A}{X}$ is closed in $X$. \end{proposition} \begin{proof} - $\closure{A}{X}\setminus\interior{A}{X}$ is closed in $X$ by \cref{closure_interior_frontier_is_in_carrier,closure_is_closed,interior_is_open,closed_minus_open_is_closed}. + $\closure{A}{X},\interior{A}{X}\subseteq\carrier[X]$ + by \cref{closure_interior_frontier_is_in_carrier}. + $\closure{A}{X}$ is closed in $X$ by \cref{closure_is_closed}. + $\interior{A}{X}$ is open in $X$ by \cref{interior_is_open}. + $\closure{A}{X}\setminus\interior{A}{X}$ is closed in $X$ + by \cref{closed_minus_open_is_closed}. + Follows by \cref{frontier}. \end{proof} \begin{proposition}\label{setdifference_eq_intersection_with_complement} Suppose $A,B \subseteq C$. Then $A \setminus B = A \inter (C \setminus B)$. \end{proposition} +\begin{proof} + Follows by \cref{setminus_eq_inter_complement}. +\end{proof} @@ -500,12 +616,13 @@ $\frontier{A}{X} = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. \end{proposition} \begin{proof} - \begin{align*} - \frontier{A}{X} \\ - &= \closure{A}{X}\setminus\interior{A}{X} \\ - &= \closure{A}{X} \inter (\carrier[X] \setminus \interior{A}{X}) \explanation{by \cref{setdifference_eq_intersection_with_complement,closure_interior_frontier_is_in_carrier}}\\ - &= \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X} \explanation{by \cref{complement_interior_eq_closure_complement}} - \end{align*} + $\closure{A}{X}\setminus\interior{A}{X} + =\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})$ + by \cref{setdifference_eq_intersection_with_complement,closure_interior_frontier_is_in_carrier}. + $\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X}) + =\closure{A}{X}\inter\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{complement_interior_eq_closure_complement}. + Follows by \cref{frontier}. \end{proof} \begin{proposition}\label{frontier_of_emptyset} @@ -513,7 +630,9 @@ Then $\frontier{\emptyset}{X} = \emptyset$. \end{proposition} \begin{proof} - Follows by set extensionality. + $\interior{\emptyset}{X}=\emptyset$ + by \cref{emptyset_open,interior_of_open}. + Follows by \cref{frontier,closure_emptyset,setminus_self}. \end{proof} \begin{proposition}\label{frontier_of_carrier} |