有限交叉
$ \forall X\forall\mathcal F\in 2^{2^X}にて、部分有限集合$ \forall\mathcal F'\subseteq\mathcal Fの共分$ \bigcap\mathcal F'が$ \bigcap\mathcal F'\neq\varnothingを満たすとき、$ \mathcal Fは(有限交叉性をもつ|有限交叉的である)という 1行で示すと
$ \mathcal Fが有限交叉的$ \iff\forall\mathcal F'\subseteq\mathcal F:(|\mathcal F'|\in\Z_{\ge0}\implies\bigcap\mathcal F'\neq\varnothing)
$ \forall n\in\N\forall F:\N_{<n}\to\mathcal F:\bigcap_{i<n}F_i\neq\varnothingのほうが使いやすいかな
補題17.1$ \forall X.(\exist\mathcal F\in2^{2^X}.\mathcal Fは有限交叉的$ )\implies X\neq\varnothing
証明
$ \forall X.
$ \exist\mathcal F\in2^{2^X}.\mathcal Fは有限交叉的
$ \iff\exist\mathcal F\in2^{2^X}\forall\mathcal F'\subseteq\mathcal F.|\mathcal F'|\in\Z_{\ge0}\land\bigcap\mathcal F'\neq\varnothing
$ \iff\exist\mathcal F\in2^{2^X}\forall\mathcal F'\subseteq\mathcal F.|\mathcal F'|\in\Z_{\ge0}\land\exist x\in X\exist F\in\mathcal F'.x\in F
$ \implies X\neq\varnothing
性質
$ \forall F\in\mathcal F.F\neq\varnothing
証明：
$ \forall\mathcal F'\subseteq\mathcal F.(|\mathcal F'|\in\Z_{\ge0}\implies\bigcap\mathcal F'\neq\varnothing)
$ \implies\forall F\in\mathcal F.(|\{F\}|\in\Z_{\ge0}\implies\bigcap\{F\}\neq\varnothing)
$ \underline{\iff\forall F\in\mathcal F.F\neq\varnothing\quad}_\blacksquare
$ \forall F_1,F_2\in\mathcal F.F_1\cap F_2\neq\varnothing
証明：
$ \forall\mathcal F'\subseteq\mathcal F.(|\mathcal F'|\in\Z_{\ge0}\implies\bigcap\mathcal F'\neq\varnothing)
$ \implies\forall F_1,F_2\in\mathcal F.(|\{F_1,F_2\}|\in\Z_{\ge0}\implies\bigcap\{F_1,F_2\}\neq\varnothing)
$ \underline{\iff\forall F_1,F_2\in\mathcal F.F_1\cap F_2\neq\varnothing\quad}_\blacksquare