∀O∀B:(∃B0⊆B:O=⋃B0)⇔(∀x∈O∃b∈B:x∈b⊆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*}

形式を整えやすくなった

複雑な数式も書きやすい

間にコメントを入れられないのがやや不便