極大filter

$ \mathcal F^*\text{ is an ultra filter of }\mathscr F_X:\iff\mathcal F^*\in\mathrm{max}^*\mathscr F_X

別名

$ \forall X\forall\mathcal F^*\in\mathscr F_X:\mathcal F^*\in\mathrm{max}^*\mathscr F_X\iff\forall A\in2^X:A\in\mathcal F^*\lor X\setminus A\in\mathcal F^*

proof

(L)⇒(R)

$ \forall X\forall\mathcal F^*\in\mathscr F_X:

$ \mathcal F^*\in\mathrm{max}^*\mathscr F_X

$ \implies\forall A\in2^X:

$ A\notin\mathcal F^*

$ \implies\mathcal F^*\subseteq\lang\left.\mathcal F^*\right|_{\setminus A}\rang_X\in\mathscr F_X

$ \because\forall X\forall A\in2^X\forall\mathcal F\in\mathscr F_X:A\notin\mathcal F\implies\mathcal F\subseteq\lang\left.\mathcal F\right|_{\setminus A}\rang_X\in\mathscr F_X

$ \implies\mathcal F^*=\lang\left.\mathcal F^*\right|_{\setminus A}\rang_X

$ \because\mathcal F^*\in\mathrm{max}^*\mathscr F_X

$ \implies X\setminus A\in\mathcal F^*

$ \underline{\implies\forall A\in2^X:A\in\mathcal F^*\lor X\setminus A\in\mathcal F^*\quad}_\blacksquare

(R)⇒(L)

$ \forall X\forall\mathcal F^*\in\mathscr F_X:

$ \forall A\in2^X:A\in\mathcal F^*\lor X\setminus A\in\mathcal F^*

$ \implies\forall\mathcal G\in\mathscr F_X:

$ \mathcal F^*\subseteq\mathcal G

$ \implies\forall A:

$ A\in\mathcal G

$ \implies A\in\mathcal G\land(X\setminus A\notin\mathcal F^*\implies A\in\mathcal F^*)

$ \implies X\setminus A\notin\mathcal G\land(X\setminus A\notin\mathcal F^*\implies A\in\mathcal F^*)

$ \implies X\setminus A\notin\mathcal F^*\land(X\setminus A\notin\mathcal F^*\implies A\in\mathcal F^*)

$ \because\mathcal F^*\subseteq\mathcal G

$ \implies A\in\mathcal F^*

$ \implies\mathcal F^*\subseteq\mathcal G\subseteq\mathcal F^*

$ \iff\mathcal F^*=\mathcal G

$ \underline{\implies\mathcal F^*\in\mathrm{max}^*\mathscr F_X\quad}_\blacksquare