Archive:
Subtopics:
Comments disabled |
Wed, 10 Nov 2021
Annoying Kuratowski pair projection formula
In a recent article I complained that it was too difficult to extract the second component from a Kuratowski pair. The formula given by Wikipedia is not simple: $$\pi_2(p) = \bigcup\left\{\left. x \in \bigcup p\,\right|\,\bigcup p \neq \bigcap p \implies x \notin \bigcap p \right\}$$ I said “It's so non-obvious that I suspect that it's wrong”. Matthijs Blom then contacted me with this formal correctness proof using the Lean theorem prover. (Raw source code.) I have also convinced myself that it is correct, using old-fashioned methods. !!\def\pr#1#2{\langle{#1},{#2}\rangle}!! !!\def\kp#1#2{\{\{{#1}\}, \{{#1},{#2}\}\}}!! Let's recall !!p = \pr ab = \kp ab!! and observe that then $$ \bigcup p = \{a, b\}\\ \bigcap p = \{a\} $$ where possibly !!a=b!!. Then the Wikipedia formula can be written as: $$\pi_2(\pr ab) = \bigcup\left\{\left. x \in \{a, b\} \,\right| \,\{a, b\} \neq \{a\} \implies x \notin \{a\} \right\}.$$ !!\{a, b\} \ne \{a\}!! can be rewritten as !!b\ne a!!. The !!x\notin\{a\}!! can be rewritten as !!x\ne a!!. We can rewrite the whole !!S\implies T!! thing as !!\lnot S\lor T!!: $$\pi_2(\pr ab) = \bigcup\left\{\left. x \in \{a, b\} \,\right| \,a = b \lor x \ne a \right\}.$$ When !!a≠b!! the !!a=b!! clause in the guard condition vanishes, leaving $$\begin{align} \pi_2(\pr ab) & = \bigcup\left\{\left. x \in \{a, b\} \,\right| \,x \ne a \right\} \\ % & = \bigcup\{ x \in \{ b\} \} \\ & = \bigcup\{b\} \\ & = b. \end{align} $$ When !!a=b!!, the !!\{a,b\}!! expression reduces to !!\{b\}!! and the guard condition !!a = b \lor x \ne a!! is always true, so we get: $$\begin{align} \pi_2(\pr ab) & = \bigcup\{ x \in \{b\}\} \\ & = \bigcup\{b\} \\ & = b. \end{align} $$ [Other articles in category /math] permanent link |