compact
典型的な定義
位相空間$ (X,\mathcal O)にて$ A\in 2^Xが以下を満たすとき、「$ Aはコンパクト」「$ Aはcompact集合」であるという $ \forall\mathcal O'\subseteq\mathcal O:A\subseteq\bigcup\mathcal O'\implies\exist\mathcal O''\subseteq\mathcal O':A\subseteq\bigcup\mathcal O''\land|\mathcal O''|\in\N
任意の位相空間$ (X,\mathcal O)と$ \forall A\in 2^Xにて以下が成り立つ
$ A \text{ is a compact set on }(X,\mathcal O)\iff (A,\left.\mathcal O\right|_{\cap A})\text{ is compact}
$ \forall\mathcal F\in\max^*\mathscr F_X\exist x\in X:\mathcal F\to x
$ \forall\mathcal F\in\max^*\mathscr F_X\exist x\in X:\mathcal N(x)\subseteq\mathcal Fとも書ける
$ (X,\mathcal O)\text{ is compact}\iff\forall\mathcal C'\subseteq\mathcal C:\left(\mathcal C'\text{は有限交叉族}\implies\bigcap\mathcal C'\neq\varnothing\right)
証明
$ (X,\mathcal O)\text{ is compact}
$ \iff\forall\mathcal O'\subseteq\mathcal O:\left(X=\bigcup\mathcal O'\implies\exist\mathcal O''\subseteq\mathcal O':X=\bigcup\mathcal O''\land|\mathcal O''|\in\N\right)
$ \iff\forall\mathcal O'\subseteq\mathcal O:\left(X\setminus X=\bigcap_{O\in\mathcal O'}(X\setminus O)\implies\exist\mathcal O''\subseteq\mathcal O':X\setminus X=\bigcap_{O\in\mathcal O''}(X\setminus O)\land|\mathcal O''|\in\N\right)
$ \iff\forall\mathcal C'\subseteq\mathcal C:\left(\varnothing=\bigcap\mathcal C'\implies\exist\mathcal C''\subseteq\mathcal C':\varnothing=\bigcap\mathcal C''\land|\mathcal C''|\in\N\right)
$ \iff\forall\mathcal C'\subseteq\mathcal C:\left(\forall\mathcal C''\subseteq\mathcal C':\left(|\mathcal C''|\in\N\implies\bigcap\mathcal C''\neq\varnothing\right)\implies\bigcap\mathcal C'\neq\varnothing\right)
$ \underline{\iff\forall\mathcal C'\subseteq\mathcal C:\left(\mathcal C'\text{は有限交叉族}\implies\bigcap\mathcal C'\neq\varnothing\right)\quad}_\blacksquare
$ (X,\mathcal O)\text{ is compact}\iff\forall\mathcal F\in\mathscr F_X\exist \mathcal F'\in\mathscr F_X\exist x\in X:\mathcal F\subseteq\mathcal F'\to x
$ \forall X\forall\mathcal F\in\mathscr F_X:\bigcap_{F\in\mathcal F}\overline{F}=\Set{x\in X|\exist G\in\mathscr F_X:\mathcal F\subseteq\mathcal G\to x}
$ \forall\mathcal F:
$ \mathcal F\in\mathscr F_X
$ \implies\mathcal F\in\mathscr F_X\land\Set{F'|\exist F\in\mathcal F:F'=\overline{F}}\text{は有限交叉族}
$ \implies\mathcal F\in\mathscr F_X\land\bigcap_{F\in\mathcal F}\overline{F}\neq\varnothing
$ \underline{\implies\exist x\in X\exist \mathcal F'\in\mathscr F_X:\mathcal F\subseteq\mathcal F'\to x\quad}_\blacksquare
$ \forall\mathcal C'\subseteq\mathcal C:
$ \mathcal C'\text{は有限交叉族}
$ \implies\left\lang\Set{C|\exist\mathcal C''\subseteq\mathcal C':C=\bigcap\mathcal C''\land|\mathcal C''|\in\N}\right\rang_X\in\mathscr F_X
$ \implies\exist x\in X\exist \mathcal F'\in\mathscr F_X:\left\lang\Set{C|\exist\mathcal C''\subseteq\mathcal C':C=\bigcap\mathcal C''\land|\mathcal C''|\in\N}\right\rang_X\subseteq\mathcal F'\to x
$ \iff\varnothing\neq\bigcap_{C\in\left\lang\Set{C|\exist\mathcal C''\subseteq\mathcal C':C=\bigcap\mathcal C''\land|\mathcal C''|\in\N}\right\rang_X}\overline{C}
$ \subseteq\bigcap\mathcal C'
TODO: これを証明するtakker.icon
$ \underline{\implies\bigcap\mathcal C'\neq\varnothing\quad}_\blacksquare