avewright/proofwiki-math huggingface dataset:
Theorem: Rule of Association/Conjunction/Formulation 2

:$\vdash \paren {p \land \paren {q \land r} } \iff \paren {\paren {p \land q} \land r}$

Proof:
=== Forward Implication ===
{{:Rule of Association/Conjunction/Formulation 2/Proof 1/Forward Implication}}
=== Reverse Implication ===
{{:Rule of Association/Conjunction/Formulation 2/Proof 1/Reverse Implication}}
{{BeginTableau|\vdash \paren {p \land \paren {q \land r} } \iff \paren {\paren {p \land q} \land r} }}
{{TheoremIntro|1|\paren {p \land \paren {q \land r} } \implies \paren {\paren {p \land q} \land r}|Forward Implication}}
{{TheoremIntro|2|\paren {p \land \paren {q \land r} } \impliedby \paren {\paren {p \land q} \land r}|Reverse Implication}}
{{BiconditionalIntro|3||\paren {p \land \paren {q \land r} } \iff \paren {\paren {p \land q} \land r}|1|2}}
{{EndTableau|qed}}
Theorem: Rule of Association/Conjunction/Formulation 2

:$\vdash \paren {p \land \paren {q \land r} } \iff \paren {\paren {p \land q} \land r}$

Proof:
{{BeginTableau|\vdash \paren {p \land \paren {q \land r} } \iff \paren {\paren {p \land q} \land r} }}
{{Assumption  |1|p \land \paren {q \land r} }}
{{SequentIntro|2|1|\paren {p \land q} \land r|1|Rule of Association: Formulation 1}}
{{Implication |3||\paren {p \land \paren {q \land r} } \implies \paren {\paren {p \land q} \land r}|1|2}}
{{Assumption  |4|\paren {p \land q} \land r}}
{{SequentIntro|5|4|p \land \paren {q \land r}|4|Rule of Association: Formulation 1}}
{{Implication |6||\paren {\paren {p \land q} \land r} \implies \paren {p \land \paren {q \land r} }|4|5}}
{{BiconditionalIntro|7||\paren {p \land \paren {q \land r} } \iff \paren {\paren {p \land q} \land r}|3|6}}
{{EndTableau|qed}}
Theorem: Rule of Association/Disjunction/Formulation 2

:$\vdash \paren {p \lor \paren {q \lor r} } \iff \paren {\paren {p \lor q} \lor r}$

Proof:
{{BeginTableau|\vdash \paren {p \lor \paren {q \lor r} } \iff \paren {\paren {p \lor q} \lor r} }}
{{Assumption  |1|p \lor \paren {q \lor r} }}
{{SequentIntro|2|1|\paren {p \lor q} \lor r|1|Rule of Association: Formulation 1}}
{{Implication |3||\paren {p \lor \paren {q \lor r} } \implies \paren {\paren {p \lor q} \lor r}|1|2}}
{{Assumption  |4|\paren {p \lor q} \lor r}}
{{SequentIntro|5|4|p \lor \paren {q \lor r}|4|Rule of Association: Formulation 1}}
{{Implication |6||\paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {q \lor r} }|4|5}}
{{BiconditionalIntro|7||\paren {p \lor \paren {q \lor r} } \iff \paren {\paren {p \lor q} \lor r}|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Association/Disjunction/Formulation 2

:$\vdash \paren {p \lor \paren {q \lor r} } \iff \paren {\paren {p \lor q} \lor r}$

Proof:
{{BeginTableau|\vdash \paren {p \lor \paren {q \lor r} } \iff \paren {\paren {p \lor q} \lor r}|Instance 2 of the Hilbert-style systems}}
{{TableauLine
 | n = 1
 | f = \paren {p \lor \paren {q \lor r} } \implies \paren {\paren {p \lor q} \lor r}
 | rlnk = Rule of Association/Disjunction/Formulation 2/Forward Implication
 | rtxt = Rule of Association: Forward Implication
}}
{{TableauLine
 | n = 2
 | f = \paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {q \lor r} }
 | rlnk = Rule of Association/Disjunction/Formulation 2/Reverse Implication
 | rtxt = Rule of Association: Reverse Implication
}}
{{TableauLine
 | n = 3
 | f = \paren {\paren {p \lor \paren {q \lor r} } \implies \paren {\paren {p \lor q} \lor r} } \land \paren {\paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {q \lor r} } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 4$
 | dep  = 1, 2
}}
{{TableauLine
 | n = 4
 | f = \paren {p \lor \paren {q \lor r} } \iff \paren {\paren {p \lor q} \lor r}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 2 (3)$
 | dep  = 3
}}
{{EndTableau}}
{{qed}}
Theorem: Principle of Commutation/Formulation 1/Forward Implication

:$p \implies \paren {q \implies r} \vdash q \implies \paren {p \implies r}$

Proof:
{{BeginTableau|p \implies \paren {q \implies r} \vdash q \implies \paren {p \implies r} }}
{{Premise|1|p \implies \paren {q \implies r} }}
{{Assumption|2|q}}
{{Assumption|3|p}}
{{ModusPonens|4|1, 3|q \implies r|1|3}}
{{ModusPonens|5|1, 2, 3|r|2|4}}
{{Implication|6|1, 2|p \implies r|3|5}}
{{Implication|7|1|q \implies \paren {p \implies r}|2|6}}
{{EndTableau|qed}}
Theorem: Principle of Commutation/Formulation 1

:$p \implies \paren {q \implies r} \dashv \vdash q \implies \paren {p \implies r}$

Proof:
{{BeginTableau|p \implies \paren {q \implies r} \vdash q \implies \paren {p \implies r} }}
{{Premise|1|p \implies \paren {q \implies r} }}
{{Assumption|2|q}}
{{Assumption|3|p}}
{{ModusPonens|4|1, 3|q \implies r|1|3}}
{{ModusPonens|5|1, 2, 3|r|2|4}}
{{Implication|6|1, 2|p \implies r|3|5}}
{{Implication|7|1|q \implies \paren {p \implies r}|2|6}}
{{EndTableau|qed}}
Theorem: Principle of Commutation/Formulation 1

:$p \implies \paren {q \implies r} \dashv \vdash q \implies \paren {p \implies r}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc||ccccc|} \hline
p & \implies & (q & \implies & r) & q & \implies & (p & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \F & \T & \T & \F & \T & \T & \T & \T \\
\T & \F & \T & \F & \F & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Principle of Commutation/Formulation 1

:$p \implies \paren {q \implies r} \dashv \vdash q \implies \paren {p \implies r}$

Proof:
{{BeginTableau|q \implies \paren {p \implies r} \vdash p \implies \paren {q \implies r} }}
{{Premise|1|q \implies \paren {p \implies r} }}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{ModusPonens|4|1, 3|p \implies r|1|3}}
{{ModusPonens|5|1, 2, 3|r|2|4}}
{{Implication|6|1, 2|q \implies r|3|5}}
{{Implication|7|1|p \implies \paren {q \implies r}|2|6}}
{{EndTableau|qed}}
Theorem: Principle of Commutation/Formulation 1/Reverse Implication

:$q \implies \paren {p \implies r} \vdash p \implies \paren {q \implies r}$

Proof:
{{BeginTableau|q \implies \paren {p \implies r} \vdash p \implies \paren {q \implies r} }}
{{Premise|1|q \implies \paren {p \implies r} }}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{ModusPonens|4|1, 3|p \implies r|1|3}}
{{ModusPonens|5|1, 2, 3|r|2|4}}
{{Implication|6|1, 2|q \implies r|3|5}}
{{Implication|7|1|p \implies \paren {q \implies r}|2|6}}
{{EndTableau|qed}}
Theorem: Principle of Commutation/Formulation 2

:$\vdash \paren {p \implies \paren {q \implies r} } \iff \paren {q \implies \paren {p \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \iff \paren {q \implies \paren {p \implies r} } }}
{{TheoremIntro|1|\paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }|Principle of Commutation: Formulation 2: Forward Implication}}
{{TheoremIntro|2|\paren {q \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|Principle of Commutation: Formulation 2: Reverse Implication}}
{{BiconditionalIntro|3||\paren {p \implies \paren {q \implies r} } \iff \paren {q \implies \paren {p \implies r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Principle of Commutation/Formulation 2

:$\vdash \paren {p \implies \paren {q \implies r} } \iff \paren {q \implies \paren {p \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} } }}
{{Assumption|1|p \implies \paren {q \implies r} }}
{{SequentIntro|2|1|q \implies \paren {p \implies r}|1|Principle of Commutation: Formulation 1: Forward Implication}}
{{Implication|3||\paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }|1|2}}
{{EndTableau|qed}}
Theorem: Principle of Commutation/Formulation 2

:$\vdash \paren {p \implies \paren {q \implies r} } \iff \paren {q \implies \paren {p \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} } }}
{{Assumption|1|p \implies \paren {q \implies r} }}
{{Assumption|2|q}}
{{Assumption|3|p}}
{{ModusPonens|4|1, 3|q \implies r|1|3}}
{{ModusPonens|5|1, 2, 3|r|2|4}}
{{Implication|6|1, 2|p \implies r|3|5}}
{{Implication|7|1|q \implies \paren {p \implies r}|2|6}}
{{Implication|8||\paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }|1|7}}
{{EndTableau|qed}}
Theorem: Principle of Commutation/Formulation 2

:$\vdash \paren {p \implies \paren {q \implies r} } \iff \paren {q \implies \paren {p \implies r} }$

Proof:
Using a tableau proof for instance 1 of a Hilbert proof system:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} } |nohead = 1}}
{{Assumption|1|p}}
{{Assumption|2|p \implies \paren {q \implies r} }}
{{ModusPonens|3|1, 2|q \implies r|1|2}}
{{Assumption|4|q}}
{{ModusPonens|5|1, 2, 4|r|3|4}}
{{TableauLine|n = 6
  | pool = 2, 4
  | f = p \implies r
  | rlnk = Definition:Deduction Rule
  | rtxt = Deduction Rule
  | dep  = 5
}}
{{TableauLine|n = 7
  | pool = 2
  | f = q \implies \paren {p \implies r}
  | rlnk = Definition:Deduction Rule
  | rtxt = Deduction Rule
  | dep  = 6
}}
{{TableauLine|n = 8
  | f = \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }
  | rlnk = Definition:Deduction Rule
  | rtxt = Deduction Rule
  | dep  = 7
}}
{{EndTableau}}
{{qed}}
Theorem: Principle of Commutation/Formulation 2

:$\vdash \paren {p \implies \paren {q \implies r} } \iff \paren {q \implies \paren {p \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {q \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption   |1|q \implies \paren {p \implies r} }}
{{SequentIntro |2|1|p \implies \paren {q \implies r}|1|Principle of Commutation: Formulation 1: Reverse Implication}}
{{Implication  |3| |\paren {q \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Principle of Commutation/Formulation 2/Forward Implication

:$\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} } }}
{{Assumption|1|p \implies \paren {q \implies r} }}
{{SequentIntro|2|1|q \implies \paren {p \implies r}|1|Principle of Commutation: Formulation 1: Forward Implication}}
{{Implication|3||\paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }|1|2}}
{{EndTableau|qed}}
Theorem: Principle of Commutation/Formulation 2/Forward Implication

:$\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} } }}
{{Assumption|1|p \implies \paren {q \implies r} }}
{{Assumption|2|q}}
{{Assumption|3|p}}
{{ModusPonens|4|1, 3|q \implies r|1|3}}
{{ModusPonens|5|1, 2, 3|r|2|4}}
{{Implication|6|1, 2|p \implies r|3|5}}
{{Implication|7|1|q \implies \paren {p \implies r}|2|6}}
{{Implication|8||\paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }|1|7}}
{{EndTableau|qed}}
Theorem: Principle of Commutation/Formulation 2/Forward Implication

:$\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }$

Proof:
Using a tableau proof for instance 1 of a Hilbert proof system:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} } |nohead = 1}}
{{Assumption|1|p}}
{{Assumption|2|p \implies \paren {q \implies r} }}
{{ModusPonens|3|1, 2|q \implies r|1|2}}
{{Assumption|4|q}}
{{ModusPonens|5|1, 2, 4|r|3|4}}
{{TableauLine|n = 6
  | pool = 2, 4
  | f = p \implies r
  | rlnk = Definition:Deduction Rule
  | rtxt = Deduction Rule
  | dep  = 5
}}
{{TableauLine|n = 7
  | pool = 2
  | f = q \implies \paren {p \implies r}
  | rlnk = Definition:Deduction Rule
  | rtxt = Deduction Rule
  | dep  = 6
}}
{{TableauLine|n = 8
  | f = \paren {p \implies \paren {q \implies r} } \implies \paren {q \implies \paren {p \implies r} }
  | rlnk = Definition:Deduction Rule
  | rtxt = Deduction Rule
  | dep  = 7
}}
{{EndTableau}}
{{qed}}
Theorem: Principle of Commutation/Formulation 2/Reverse Implication

:$\vdash \paren {q \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {q \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption   |1|q \implies \paren {p \implies r} }}
{{SequentIntro |2|1|p \implies \paren {q \implies r}|1|Principle of Commutation: Formulation 1: Reverse Implication}}
{{Implication  |3| |\paren {q \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Linearly Ordered Space is Connected iff Linear Continuum

Let $T = \struct {S, \preceq, \tau}$ be a linearly ordered space.
Then $S$ is a connected space {{iff}} it is a linear continuum.

Proof:
{{explain|It is not clear how the premises of the subproofs (e.g. "$T$ is disconnected and densely ordered" directly relate to the premises of the main theorem, e.g.: "$S$ is a connected space..."}}
Theorem: Rule of Transposition/Variant 1/Formulation 2/Forward Implication

:$\vdash \paren {p \implies \neg q} \implies \paren {q \implies \neg p}$

Proof:
{{BeginTableau|\vdash \paren {p \implies \neg q} \implies \paren {q \implies \neg p} }}
{{Assumption|1|p \implies \neg q}}
{{Assumption|2|q}}
{{DoubleNegIntro|3|2|\neg \neg q|2}}
{{ModusTollens|4|1, 2|\neg p|1|3}}
{{Implication|5|1|q \implies \neg p|2|4}}
{{Implication|6||\paren {p \implies \neg q} \implies \paren {q \implies \neg p}|1|5}}
{{EndTableau}}
{{Qed}}
Theorem: Boundary of Polygon is Jordan Curve

Let $P$ be a polygon embedded in $\R^2$.
Then there exists a Jordan curve $\gamma: \closedint 0 1 \to \R^2$ such that the image of $\gamma$ is equal to the boundary $\partial P$ of $P$.

Proof:
The polygon $P$ has $n$ sides, where $n \in \N$.
Denote the vertices of $P$ as $A_1, \ldots, A_n$ and its sides as $S_1, \ldots, S_n$, such that each vertex $A_i$ has adjacent sides $S_{i - 1}$ and $S_i$.
We use the conventions that $S_0 = S_n$, and $A_{n + 1} = A_1$.
As each side $S_i$ is a line segment joining $A_i$ and $A_{i + 1}$, when we define the path $\gamma_i: \closedint 0 1 \to \R^2$ by:
:$\map {\gamma_i} t = \paren {1 - t} A_i + t A_{i + 1}$
the image of $\gamma_i$ is equal to the side $S_i$.
Define $\gamma: \closedint 0 1 \to \R^2$ as the concatenation $\paren {\cdots \paren {\paren {\gamma_1 * \gamma_2} * \gamma_3} * \ldots * \gamma_{n - 1} } * \gamma_n$.
Then each point in the image of $\gamma$ corresponds to a point in a side of $P$.
As $\map \gamma 0 = A_1 = \map \gamma 1$ by our definition of $A_{n + 1}$, it follows that $\gamma$ is a closed path.
It follows from the definition of polygon that the sides of $P$ do not intersect, except at the vertices.
For $i \ne 1$, each vertex $A_i$ is the initial point of $\gamma_i$ and the final point of $\gamma_{i - 1}$, and is equal to exactly one point $\map \gamma {2^{-n - 1 + i} }$ in the image of $\gamma$.
Then we have that $\gamma$ restricted to $\hointr 0 1$ is injective.
Hence $\gamma$ is a Jordan curve.
{{qed}}
Category:Jordan Curves
9lrfy3ociyg3k8oyk5pyzzv8dqrv55s
Theorem: Rule of Explosion/Variant 1

:$\vdash p \implies \paren {\neg p \implies q}$

Proof:
{{BeginTableau|\vdash p \implies \paren {\neg p \implies q} }}
{{Assumption|1|p}}
{{Assumption|2|\neg p}}
{{NonContradiction|3|1, 2|1|2}}
{{Explosion|4|1, 2|q|3}}
{{Implication|5|1|\neg p \implies q|2|4}}
{{Implication|6||p \implies \paren {\neg p \implies q}|1|5}}
{{EndTableau|qed}}
Theorem: Negation of Conditional implies Antecedent

:$\vdash \neg \paren {p \implies q} \implies p$

Proof:
{{BeginTableau|\vdash \neg \paren {p \implies q} \implies p}}
{{Assumption|1|\neg \paren {p \implies q} }}
{{Assumption|2|\neg \paren {p \land \neg q} }}
{{SequentIntro|3|2|p \implies q|2|Conditional is Equivalent to Negation of Conjunction with Negative}}
{{NonContradiction|4|1, 2|3|1}}
{{Reductio|5|1|p \land \neg q|2|4}}
{{Simplification|6|1|p|5|1}}
{{Implication|7||\neg \paren {p \implies q} \implies p|1|6}}
{{EndTableau|qed}}
Theorem: Negation of Conditional implies Antecedent

:$\vdash \neg \paren {p \implies q} \implies p$

Proof:
{{BeginTableau|\vdash \neg \paren {p \implies q} \implies p}}
{{Assumption|1|\neg \paren {p \implies q} }}
{{SequentIntro|2|1|p \land \neg q|1|Conjunction with Negative is Equivalent to Negation of Conditional}}
{{Simplification|3|1|p|2|1}}
{{Implication|4||\neg \paren {p \implies q} \implies p|1|3}}
{{EndTableau|qed}}
Theorem: Negation of Conditional implies Negation of Consequent

:$\vdash \neg \paren {p \implies q} \implies \neg q$

Proof:
{{BeginTableau|\vdash \neg \paren {p \implies q} \implies \neg q}}
{{Assumption|1|\neg \paren {p \implies q} }}
{{Assumption|2|\neg \paren {p \land \neg q} }}
{{SequentIntro|3|2|p \implies q|2|Conditional is Equivalent to Negation of Conjunction with Negative}}
{{NonContradiction|4|1, 2|3|1}}
{{Reductio|5|1|p \land \neg q|2|4}}
{{Simplification|6|1|\neg q|5|2}}
{{Implication|7||\neg \paren {p \implies q} \implies \neg q|1|7}}
{{EndTableau|qed}}
Theorem: Negation of Conditional implies Negation of Consequent

:$\vdash \neg \paren {p \implies q} \implies \neg q$

Proof:
{{BeginTableau|\vdash \neg \paren {p \implies q} \implies \neg q}}
{{Assumption|1|\neg \paren {p \implies q} }}
{{SequentIntro|2|1|p \land \neg q|1|Conjunction with Negative is Equivalent to Negation of Conditional}}
{{Simplification|3|1|\neg q|2|2}}
{{Implication|4||\neg \paren {p \implies q} \implies \neg q|1|3}}
{{EndTableau|qed}}
Theorem: Matrix Multiplication Interpretation of Relation Composition

Let $A$, $B$ and $C$ be finite non-empty sets that are initial segments of $\N_{\ne 0}$.
Let $\RR \subseteq B \times A$ and $\SS \subseteq C \times B$ be relations.
Let $\mathbf R$ and $\mathbf S$ be matrices which we define as follows:
:$\sqbrk r_{i j} = \begin{cases}
\T & : \tuple {i, j} \in \RR \\
\F & : \tuple {i, j} \notin \RR \\
\end{cases}$
:$\sqbrk s_{i j} = \begin{cases}
\T & : \tuple {i, j} \in \SS \\
\F & : \tuple {i, j} \notin \SS \\
\end{cases}$
Then we can interpret the matrix product $\mathbf R \mathbf S$ as the composition $\SS \circ \RR$.
To do so we temporarily consider $\struct {\set {\T, \F}, \land, \lor}$ to be our "ring" on which we are basing matrix multiplication.
Then:
:$\sqbrk {r s}_{i j} = \T \iff \tuple {i, j} \in \SS \circ \RR$

Proof:
=== Sufficient Condition ===
Suppose for some $i, j$:
:$\sqbrk {r s}_{i j} = \T$
Then by definition of $\lor$ there must exist some $k$ for which:
:$\sqbrk r_{i k} \land \sqbrk s_{k j} = \T$
which by our definition implies:
:$\tuple {i, k} \in \RR$
:$\tuple {k, j} \in \SS$
Then by definition of a composite relation:
:$\tuple {i, j} \in \RR \circ \SS$
Theorem: Space is Compact iff Every Cover from Basis has Finite Subcover

Let $T = \struct {S, \tau}$ be a topological space.
Let $\BB \subseteq \tau$ be a basis of $\tau$.
Then $T = \struct {S, \tau}$ is '''compact''' {{iff}}:
:from every cover of $S$ by elements of $\BB$, a finite subcover of $S$ can be selected.

Proof:
=== Sufficient Condition ===
Let every open cover for $S$ have a finite subcover.
Then every cover of $S$ by elements of $\BB$ is an open cover for $S$.
So:
:from every cover of $S$ by elements of $\BB$, a finite subcover of $S$ can be selected.
{{qed|lemma}}
Theorem: Set of Subsets is Cover iff Set of Complements is Free

Let $S$ be a set.
Let $\CC$ be a set of sets.
Then $\CC$ is a cover for $S$ {{iff}} $\set {\relcomp S X: X \in \CC}$ is free.

Proof:
Let $S$ be a set.
Let us recall the definition of free:
{{:Definition:Free Set of Sets}}
Theorem: Conditional is Equivalent to Negation of Conjunction with Negative/Formulation 2/Reverse Implication

:$\vdash \paren {\neg \paren {p \land \neg q} } \implies \paren {p \implies q}$

Proof:
{{BeginTableau|\vdash \paren {\neg \paren {p \land \neg q} } \implies \paren {p \implies q} }}
{{Assumption|1|\neg \paren {p \land \neg q} }}
{{SequentIntro|2|1|p \implies q|1|Conditional is Equivalent to Negation of Conjunction with Negative: Formulation 1}}
{{Implication|3||\paren {\neg \paren {p \land \neg q} } \implies \paren {p \implies q}|1|2}}
{{EndTableau|qed}}
{{LEM|Conditional is Equivalent to Negation of Conjunction with Negative/Formulation 1/Reverse Implication|3}}
Category:Conditional is Equivalent to Negation of Conjunction with Negative
mw6xmh7o194qtrpwhw6p0y4klr6nuc1
Theorem: Biconditional Elimination

The '''rule of biconditional elimination''' is a valid argument in types of logic dealing with conditionals $\implies$ and biconditionals $\iff$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
{{:Biconditional Elimination/Proof Rule}}
=== Sequent Form ===
{{:Biconditional Elimination/Sequent Form}}

Proof:
=== Form 1 ===
{{:Biconditional Elimination/Sequent Form/Proof 1/Form 1}}
=== Form 2 ===
{{:Biconditional Elimination/Sequent Form/Proof 1/Form 2}}
Theorem: Biconditional Elimination

The '''rule of biconditional elimination''' is a valid argument in types of logic dealing with conditionals $\implies$ and biconditionals $\iff$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
{{:Biconditional Elimination/Proof Rule}}
=== Sequent Form ===
{{:Biconditional Elimination/Sequent Form}}

Proof:
We apply the Method of Truth Tables.
$\begin{array}{|ccc||ccc|ccc|} \hline
p & \iff & q & p & \implies & q & q & \implies & p \\
\hline
\F & \T & \F & \F & \T & \F & \F & \T & \F \\
\F & \F & \T & \F & \T & \T & \T & \F & \F \\
\T & \F & \F & \T & \F & \F & \F & \T & \T \\
\T & \T & \T & \T & \F & \T & \T & \T & \T \\
\hline
\end{array}$
As can be seen, when $p \iff q$ is true so are both $p \implies q$ and $q \implies p$.
{{qed}}
Theorem: Biconditional Introduction/Sequent Form

{{begin-eqn}}
{{eqn | l = p
      | o = \implies
      | r = q
}}
{{eqn | l = q
      | o = \implies
      | r = p
}}
{{eqn | ll= \vdash
      | l = p
      | o = \iff
      | r = q
}}
{{end-eqn}}

Proof:
{{BeginTableau|p \implies q, q \implies p \vdash p \iff q}}
{{Premise|1|p \implies q}}
{{Premise|2|q \implies p}}
{{BiconditionalIntro|3|1, 2|p \iff q|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Biconditional Introduction/Sequent Form

{{begin-eqn}}
{{eqn | l = p
      | o = \implies
      | r = q
}}
{{eqn | l = q
      | o = \implies
      | r = p
}}
{{eqn | ll= \vdash
      | l = p
      | o = \iff
      | r = q
}}
{{end-eqn}}

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin {array} {|ccccccc||ccc|} \hline
(p & \implies & q) & \land & (q & \implies & p) & p & \iff & q\\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \T & \F \\
\F & \T & \T & \F & \T & \F & \F & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
As can be seen, only when both $p \implies q$ and $q \implies p$ are true, then so is $p \iff q$.
{{qed}}
Theorem: Biconditional Elimination/Sequent Form/Proof 1/Form 1

:$p \iff q \vdash p \implies q$

Proof:
{{BeginTableau|p \iff q \vdash p \implies q}}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|2|1|p \implies q|1|1}}
{{EndTableau}}
{{Qed}}
Theorem: Biconditional Elimination/Sequent Form/Proof 1/Form 2

:$p \iff q \vdash q \implies p$

Proof:
{{BeginTableau|p \iff q \vdash q \implies p}}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|2|1|q \implies p|1|2}}
{{EndTableau}}
{{Qed}}