擬開核の公理→filter場の公理

$ \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}\implies\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}

証明

$ x\in X

$ \iff x\in X^\circ

$ \iff X\in\mathcal F(x)

$ \implies\mathcal F(x)\neq\varnothing

$ \underline{\therefore\forall x\in X:\mathcal F(x)\neq\varnothing\quad}_\blacksquare

$ F\in\mathcal F(x)

$ \iff x\in F^\circ\land F\in2^X

$ \implies x\in F

$ \underline{\therefore\forall x\in X:x\in\bigcap\mathcal F(x)\quad}_\blacksquare

$ F_1,F_2\in\mathcal F(x)

$ \iff x\in {F_1}^\circ\cap{F_2}^\circ\land F_1,F_2\in2^X

$ \implies x\in(F_1\cap F_2)^\circ\land F_1\cap F_2\in2^X

$ \iff F_1\cap F_2\in\mathcal F(x)

$ \implies F_1\cap F_2\in\lang\mathcal F(x)\rang_X

$ \underline{\therefore\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\quad}_\blacksquare

$ F\in\lang\mathcal F(x)\rang_X

$ \iff\exist F'\subseteq F\subseteq X:F'\in\mathcal F(x)

$ \iff\exist F'\subseteq F\subseteq X:x\in {F'}^\circ

$ \iff\exist F':\begin{dcases}F\in2^X\\F'=F'\cap F\\x\in{F'}^\circ\end{dcases}

$ \implies\exist F':\begin{dcases}F\in2^X\\x\in{F'}^\circ=(F'\cap F)^\circ\end{dcases}

$ \iff\exist F':\begin{dcases}F\in2^X\\x\in{F'}^\circ={F'}^\circ\cap F^\circ\end{dcases}

$ \iff\exist F':\begin{dcases}F\in2^X\\x\in{F'}^\circ\subseteq F^\circ\end{dcases}

$ \implies F\in2^X\land x\in F^\circ

$ \iff F\in\mathcal F(x)

$ \underline{\therefore\forall x\in X:\lang\mathcal F(x)\rang_X\subseteq\mathcal F(x)\quad}_\blacksquare

$ x\in A^\circ

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

$ \iff x\in X\land A\in\mathcal F(x)

$ \iff x\in\Set{x\in X| A\in\mathcal F(x)}

$ \underline{\therefore\forall A\in2^X:A^\circ=\Set{x\in X| A\in\mathcal F(x)}\quad}_\blacksquare