開核と閉包の相互変換

$ \because\forall x:

$ x\in\overline{X\setminus A}

$ \iff\forall C\in\mathcal C:(X\setminus A\subseteq C\implies x\in C)

$ \iff\forall C\in\mathcal C:(X\setminus C\subseteq X\setminus(X\setminus A)\implies x\in C)

$ \iff\forall C\in\mathcal C:(X\setminus C\subseteq A\implies x\in C)

$ \iff\forall C\in2^X:(X\setminus C\in\mathcal O\cap2^A\implies x\in C)

$ \iff\forall O\in2^X:(O\in\mathcal O\cap2^A\implies x\in X\setminus O)

$ \iff \forall O\in\mathcal O:(O\subseteq A\implies x\in X\land x\notin O)

$ \iff\lnot\exist O\in\mathcal O:(O\subseteq A\land(x\notin X\lor x\in O))

$ \iff\lnot(\exist O\in\mathcal O:(O\subseteq A\land x\notin X)\lor\exist O\in\mathcal O:(x\in O\subseteq A))

$ \iff\lnot((x\notin X\land\exist O\in\mathcal O:O\subseteq A)\lor x\in A^\circ)

$ \iff\lnot(x\notin X\lor x\in A^\circ)

$ \because \varnothing\in\mathcal O\land\varnothing\subseteq A

$ \iff x\in X\setminus A^\circ

$ x\in\overline{X\setminus A}

$ = \min\{C\in\mathcal C\mid X\setminus A\subseteq C\}

$ =\min\{C\in2^X\mid X\setminus C\subseteq A\land X\setminus C\in\mathcal O\}

$ \iff\exist M\in2^X:\mathcal O\ni X\setminus M\subseteq A\land\forall C\in2^X:(\mathcal O\ni X\setminus C\subseteq A\implies M\subseteq C)

$ \iff\exist M\in2^X:X\setminus A\subseteq M\in\mathcal O\land\forall C\in2^X:(\mathcal O\ni X\setminus C\subseteq A\implies X\setminus C\subseteq M)

$ \iff\exist M\in\mathcal O:X\setminus A\subseteq M\land\forall O\in\mathcal O:(X\setminus A\subseteq O\implies O\subseteq M)

$ \because \forall x:

$ x\in(X\setminus A)^\circ

$ \iff\exist O\in\mathcal O:x\in O\subseteq X\setminus A

$ \iff\exist C\in\mathcal2^X:x\in X\setminus C\in\mathcal O\land X\setminus C\subseteq X\setminus A

$ \iff\exist C\in\mathcal C:x\in X\setminus C\subseteq X\setminus A

$ \iff\exist C\in\mathcal C:x\in X\setminus C\land A\subseteq C

$ \iff x\in X\land\exist C\in\mathcal C:A\subseteq C\land x\notin C

$ \iff x\in X\land x\notin\overline A

$ \iff x\in X\setminus\overline A