filter場の公理→擬開核の公理
filter場$ \mathcal F:X\to2^{2^X}から擬開核$ \bullet^\circ:2^X\to2^Xを構成できる $ \begin{dcases}\text{(N1) }\forall x\in X:\mathcal F(x)\neq\varnothing\\\text{(N2) }\forall x\in X:x\in\bigcap\mathcal F(x)\\\text{(N3a) }\forall x\in X\forall F_1,F_2\in\mathcal F(x):F_1\cap F_2\in\lang\mathcal F(x)\rang_X\\\text{(N3b) }\forall x\in X:\lang\mathcal F(x)\rang_X\subseteq\mathcal F(x)\\\text{(N0) }\bullet^\circ:2^X\ni A\mapsto\Set{x\in X|A\in\mathcal F(x)}\in2^X\end{dcases}\implies\begin{dcases}\text{(I1) }X^\circ =X\\\text{(I2) }\forall A\in2^X:A^\circ\subseteq A\\\text{(I3) }\forall A,B\in2^X:(A\cap B)^\circ=A^\circ\cap B^\circ\\\text{(I0) }\mathcal F:X\ni x\mapsto\Set{A\in2^X|x\in A^\circ}\in2^{2^X}\end{dcases}
$ \lang\bullet\rang_\bullet：拡張 (集合) 証明
(I1)$ \forall x:
$ x\in X^\circ
$ \iff x\in X\land X\in\mathcal F(x)
$ \because(N0)
$ \implies x\in X
$ \implies x\in X\land\mathcal F(x)\neq\varnothing
$ \because(N1)
$ \implies x\in X\in\lang\mathcal F(x)\rang_X
$ \implies x\in X\in\mathcal F(x)
$ \iff x\in X^\circ
$ \because(N0)
$ \underline{\therefore X^\circ=X\quad}_\blacksquare
(I2)$ \forall A\in2^X\forall x:
$ x\in A^\circ
$ \iff x\in X\land A\in\mathcal F(x)
$ \because(N0)
$ \implies x\in A
$ \because(N2)
$ \underline{\because\forall A\in2^X:A^\circ\subseteq A\quad}_\blacksquare
(I3)$ \forall A,B\in2^X:
$ (A\cap B)^\circ=\Set{x\in X|A\cap B\in\mathcal F(x)}
$ \because(N0)
$ =\Set{x\in X|A\in\mathcal F(x)\land B\in\mathcal F(x)}
ここで、$ \text{(N3a)}\land\text{(N3b)}\implies\forall x\in X\forall F_1,F_2:(F_1,F_2\in\mathcal F(x)\iff F_1\cap F_2\in\mathcal F(x))という式を使っている
$ =A^\circ\cap B^\circ
$ \because(N0)
$ \underline{\therefore\forall A,B\in2^X:(A\cap B)^\circ=A^\circ\cap B^\circ\quad}_\blacksquare
(I0)$ \forall x\in X\forall A:
$ A\in\mathcal F(x)
$ \iff x\in X\land A\in\mathcal F(x)\subseteq 2^X
$ \iff x\in A^\circ\land A\in2^X
$ \underline{\therefore\forall x\in X:\mathcal F(x)=\Set{A\in2^X|x\in A^\circ}\quad}_\blacksquare