Definition of basis for a topology on $X$ given in the Foundation of Topology By Patty given by
Let $(X,\mathscr T)$ be a topological space. A basis for $\mathscr T$ is a subcollection $\mathscr B$ of $\mathscr T$ with the property that if $U\in \mathscr T$ then $U=\emptyset$ or there is a subcollection $\mathscr B'$ such that $U=\bigcup \{B:B\in \mathscr B'\}$
How do I write the definition of basis for the family of closed sets?
My attempt:-
Let $(X,\mathscr U)$ be a family of closed sets(closed sets of topology on $X$). A basis for $\mathscr U$ is a subcollection $\mathscr D$ of $\mathscr U$ with the property that if $D\in \mathscr U$ then $D=X$ or there is a subcollection $\mathscr D'$ such that $D=\bigcap \{D:D\in \mathscr D'\}$
am I correct?
My next aim is to prove the following Result. This result I have seen in the answer given by Brian M Scott.
A family $\mathscr X\subseteq\wp(X)$ is a base for the closed sets of topology on $X$ iff
- $\bigcap_{D\in \mathscr X} D=\varnothing$, and
- if $D_0,D_1\in\mathscr X$ and $x\notin D_0\cup D_1$, then there is a $D_2\in\mathscr X$ such that $x\notin D_2\supseteq D_0\cup D_1$.
My attempt for the proof:-
Suppose A family $\mathscr X\subseteq\wp(X)$ is a base for the closed sets of topology on $X.$
claim 1:- $\bigcap_{D\in \mathscr X} D=\varnothing$
$\varnothing \in \mathscr U$. so by the definition of basis there is a subcollection $\mathscr X'$: $\varnothing=\bigcap \{C:C\in \mathscr X'\}$. Hence,$\bigcap_{D\in \mathscr X} D=\varnothing.$
Claim 2:-if $D_0,D_1\in\mathscr X$ and $x\notin D_0\cup D_1$, then there is a $D_2\in\mathscr X$ such that $x\notin D_2\supseteq D_0\cup D_1$
if $D_0,D_1\in\mathscr X \implies D_0,D_1\in \mathscr U \implies D_0 \cup D_1 \in \mathscr U \implies \exists \mathscr X'':D_0 \cup D_1 =\bigcap \{C:C\in \mathscr X''\}. $ If $x\notin D_0 \cup D_1 \implies \exists C'\in \mathscr X'': x \notin C'.$
Conversely suppose family of subsets $\mathscr X$ satisfies the following
I. $\bigcap_{D\in \mathscr X} D=\varnothing$, and
II. if $D_0,D_1\in\mathscr X$ and $x\notin D_0\cup D_1$, then there is a $D_2\in\mathscr X$ such that $x\notin D_2\supseteq D_0\cup D_1$.
Claim:-A family $\mathscr X\subseteq\wp(X)$ is a base for the closed sets of topology on $X$. Let $\mathscr U$ is a subcollection of $\wp(X)$ consisting of $X$ and those sets are the intersection of members of $\mathscr X$. Our aim is to prove $\mathscr U$ is topology of closed sets on $x$.
(a)$X\in \mathscr U(\because \text{ by the definition of} \mathscr U$). $\emptyset \in \mathscr U (\because \text{ by the definition of} \mathscr U $ and (I)).
(b)Arbitrary intersection of closed set lie in the $\mathscr U$ immediately.
(c)How do I prove the finite union of elements of $\mathscr U$ lie in $\mathscr U$?
Let $\mathscr D$ be the basis for closed sets that we are working with.
If $A\cup B$, then there is nothing to prove. So let us assume that $X\setminus (A\cup B)\ne\emptyset$.
Then we have $A=\bigcap \mathscr D'_0$, $B=\bigcap \mathscr D'_1$ for some $\mathscr D'_{0,1}\subseteq\mathscr D$.
Let us now take the set $$S=\{(x,D_0,D_1,D_2); D_2\in\mathscr D, x\in X, x\notin D_2; D_0\cup D_1\subseteq D_2, D_0\in\mathscr D'_0, D_1\in\mathscr D'_1\}.$$ We want to show that $$A\cup B=\bigcap \{D_2; (x,D_0,D_1,D_2)\in S\text{ for some }x, D_0, D_1\}=:C.$$
Since for every $D_2$ as above we have $D_2\supseteq D_0 \supseteq A$, we get $C\supseteq A$. By the same reasoning we have $C\supseteq B$ and, consequently, $C\supseteq A\cup B$.
It remains to show that $C\subseteq A\cup B$. Assume that, on the contrary, there exists $x\in C$ such that $x\notin A\cup B$. But since $x\notin A\cup B$ we have $x\notin D_0$ and $x\notin D_1$ for some $D_0\in\mathscr D'_0$, $D_1\in\mathscr D'_1$. Therefore there exists $D_2\in\mathscr D$ such that $x\notin D_2$ and $D_0\cup D_1\subseteq D_2$. But then $(x,D_0,D_1,D_2)\in S$, and from $x\notin D_2$ we get $x\notin C$.