(∃B0⊆B:O=⋃B0)⇔(∀x∈O∃b∈B:x∈b⊆O)
$ \forall O\forall\mathcal Bにて$ (\exist\mathcal B_0\subseteq\mathcal B:O=\bigcup\mathcal B_0)\iff(\forall x\in O\exist B\in\mathcal B:x\in B\subseteq O)が成立する
証明
$ L\implies R
code:L→R.tex
\begin{align}
& \exist\mathcal B_0\subseteq\mathcal B:O=\bigcup\mathcal B_0\\
\iff & \exist\mathcal B_0\subseteq\mathcal B\forall x:(x\in O\iff\exist B\in\mathcal B_0:x\in B)\\
\iff & \exist\mathcal B_0\subseteq\mathcal B:\\
& \begin{dcases}
\forall x\in O\exist B\in\mathcal B_0:x\in B\\
\forall x:((\exist B\in\mathcal B_0:x\in B)\implies x\in O)
\end{dcases}\\
\iff & \exist\mathcal B_0\subseteq\mathcal B:\\
& \begin{dcases}
\forall x\in O\exist B\in\mathcal B_0:x\in B\\
\forall x\forall B\in\mathcal B_0:(x\in B\implies x\in O)
\end{dcases}\\
\iff & \exist\mathcal B_0\subseteq\mathcal B:\\
& \begin{dcases}
\forall x\in O\exist B\in\mathcal B_0:x\in B\\
\forall B\in\mathcal B_0:B\subseteq O
\end{dcases}\\
\implies & \exist\mathcal B_0\subseteq\mathcal B\forall x\in O\exist B\in\mathcal B_0:x\in B\subseteq O\\
\implies & \underline{\forall x\in O\exist B\in\mathcal B:x\in B\subseteq O\quad}_\blacksquare
\end{align}
$ L\impliedby R
code:R→L.tex
\begin{align*}
& \forall x\in O\exist B\in\mathcal B:x\in B\subseteq O\\
\iff & \forall x\in O\exist B\in\mathcal B_{\subseteq O}:x\in B\\
\iff & O\subseteq\bigcup\mathcal B_{\subseteq O}\\
& \quad=\bigcup(\mathcal B\cap2^O)\\
& \quad\subseteq\bigcup2^O\\
& \quad=O\\
\iff & O=\bigcup\mathcal B_{\subseteq O}\\
\implies & \underline{\exist\mathcal B_0\subseteq\mathcal B:O=\bigcup\mathcal B_0\quad}_\blacksquare
\end{align*}
形式を整えやすくなった
複雑な数式も書きやすい
間にコメントを入れられないのがやや不便