Kuratowskiの閉包公理系→開集合系の公理
Kuratowskiの閉包公理系\land \mathcal O=\{O\in2^X\mid\overline{X\setminus O}=X\setminus O\}から
開集合系の公理\land\forall A\in2^X:\overline{A}=\min\{C\in2^X\mid A\subseteq C\land X\setminus C\in\mathcal O\}を導ける
証明
(O1)
\iff\overline{X\setminus X}=X\setminus X
\underline{\iff X\in\mathcal O\quad}_\blacksquare
(O2)\forall O_1,O_2:
O_1,O_2\in\mathcal O
\iff\overline{X\setminus O_1}=X\setminus O_1\land\overline{X\setminus O_2}=X\setminus O_2
\implies\overline{X\setminus (O_1\cap O_2)}=\overline{(X\setminus O_1)\cup(X\setminus O_2)}
= \overline{X\setminus O_1}\cup\overline{X\setminus O_2}
=(X\setminus O_1)\cup(X\setminus O_2)
\because\overline{X\setminus O_1}=X\setminus O_1\land\overline{X\setminus O_2}=X\setminus O_2
=X\setminus(O_1\cap O_2)
\underline{\implies O_1\cap O_2\in\mathcal O\quad}_\blacksquare
(O3)\forall\mathcal O':
\mathcal O'\subseteq\mathcal O
\implies\forall O\in\mathcal O':O\subseteq\bigcup\mathcal O'
\implies\forall O\in\mathcal O':X\setminus\bigcup\mathcal O'\subseteq X\setminus O
\implies\forall O\in\mathcal O':\overline{X\setminus\bigcup\mathcal O'}\subseteq\overline{X\setminus O}
\implies\forall O\in\mathcal O':\overline{X\setminus\bigcup\mathcal O'}\subseteq X\setminus O
\because O\in\mathcal O'\subseteq\mathcal O
\implies\overline{X\setminus\bigcup\mathcal O'}\subseteq\bigcap_{O\in\mathcal O'}X\setminus O
=X\setminus\bigcup\mathcal O'
\subseteq\overline{X\setminus\bigcup\mathcal O'}
\underline{\implies\bigcup\mathcal O'\in\mathcal O\quad}_\blacksquare
\forall x:
x\in\min\{C\in2^X\mid A\subseteq C\land X\setminus C\in\mathcal O\}
\iff\exist M\in2^X:x\in M\land A\subseteq M\land X\setminus M\in\mathcal O\land\forall C\in2^X:(A\subseteq C\land X\setminus C\in\mathcal O\implies M\subseteq C)
\iff\exist M\in2^X:x\in M\land A\subseteq\overline M=M\land\forall C\in2^X:(A\subseteq\overline C=C\implies M\subseteq C)
\iff\exist M\in2^X:x\in M\land A\subseteq \overline{M}=M\subseteq\overline{A}\land\forall C\in2^X:(A\subseteq\overline C=C\implies M\subseteq C)
\iff\exist M\in2^X:x\in M\land A\subseteq \overline{M}=M\subseteq\overline{A}\subseteq\overline{M}\land\forall C\in2^X:(A\subseteq\overline C=C\implies M\subseteq C)
\iff\exist M\in2^X:x\in M\land A\subseteq \overline{M}=M=\overline{A}\land\forall C\in2^X:(A\subseteq\overline C=C\implies M\subseteq C)
\iff x\in\overline{A}\land\forall C\in2^X:(A\subseteq\overline C=C\implies \overline{A}\subseteq C)
\iff x\in\overline{A}
\underline{\therefore\forall A\in2^X:\overline{A}=\min\{C\in2^X\mid A\subseteq C\land X\setminus C\in\mathcal O\}\quad}_\blacksquare