avewright/proofwiki-math huggingface dataset:
Theorem: Inverse of Identity Mapping

Let $S$ be a set.
Let $I_S: S \to S$ be the identity mapping on $S$.
Then the inverse of $I_S$ is itself:
:$\paren {I_S}^{-1} = I_S$

Proof:
From the nature of the identity mapping, we have:
:$I_S \circ I_S = I_S$
from which it follows by definition that $I_S$ is the inverse of itself.
{{Qed}}
Theorem: Factoring Mapping into Quotient and Injection

Let $f: S \to T$ be a mapping.
Then $f$ can be uniquely '''factored into''' a quotient mapping, followed by an injection.
Thus:
:$f = h \circ q_{\RR_f}$
where:
:$q_{\RR_f}: S \to S / \RR_f: \map {q_{\RR_f} } s = \eqclass s {\RR_f}$
:$h: S / \RR_f \to T: \map h {\eqclass s {\RR_f} } = \map f s$
:$\eqclass s {\RR_f}$ denotes the equivalence class of $s$ with respect to the equivalence relation $\RR$ induced on $S$ by $f$.
This can be illustrated using a commutative diagram as follows:
$\quad\quad \begin{xy}\xymatrix@L+2mu@+1em{
S \ar[r]^*{q_{\RR_f} }
\ar@{-->}[rd]_*{f = h \circ q_{\RR_f} }
&
S / \RR_f \ar[d]^*{h}
\\ &
T
}\end{xy}$

Proof:
The mapping $q_{\RR_f}: S \to S / \RR_f$ follows from the definition of quotient mapping.
The mapping $h$ is justified by Condition for Mapping from Quotient Set to be Well-Defined.
{{qed}}
Theorem: Subsets in Increasing Union

Let $S_0, S_1, S_2, \ldots, S_i, \ldots$ be a nested sequence of sets, that is:
:$S_0 \subseteq S_1 \subseteq S_2 \subseteq \ldots \subseteq S_i \subseteq \ldots$
Let $S$ be the increasing union of $S_0, S_1, S_2, \ldots, S_i, \ldots$:
:$\ds S = \bigcup_{i \mathop \in \N} S_i$
Then:
:$\forall s \in S: \exists k \in \N: \forall j \ge k: s \in S_j$

Proof:
Let $k \in \N$.
Let $j \ge k$.
Then by as many applications as necessary of Subset Relation is Transitive, we have:
:$S_k \subseteq S_j$
Now $s \in S$ means, by definition of set union, that:
:$\exists S_k \subseteq S: s \in S_k$
Then from above:
:$j \ge k \implies S_k \subseteq S_j$
it follows directly that:
:$\forall s \in S: \exists k \in \N: \forall j \ge k: s \in S_j$
from the definition of subset.
{{qed}}
Theorem: Mapping on Increasing Union

Let $S_0, S_1, S_2, \ldots, S_i, \ldots$ be sets such that:
:$S_0 \subseteq S_1 \subseteq S_2 \subseteq \ldots \subseteq S_i \subseteq \ldots$
that is, each set is contained in the next as a subset.
Let $S$ be the increasing union of $S_0, S_1, S_2, \ldots, S_i, \ldots$:
:$\ds S = \bigcup_{i \mathop \in \N} S_i$
For each $i \in \N$, let $f_i: S_i \to T$ be a mapping such that:
:$\forall j < i: f_i \restriction_{S_j} = f_j$
where $f_i \restriction_{S_j}$ denotes the restriction of $f_i$ to $S_j$.
Then there is a '''unique''' mapping:
:$f: S \to T$
which extends each $f_i$ to $S$.

Proof:
Suppose $f: S \to T$ and $g: S \to T$ are both extensions of $f_i$ to $S$ for all $i \in \N$ such that $f \ne g$.
We have been given the domain and codomain of $f$.
Suppose there exists any $g: S \to T$ which is different from $f$.
This must be because $f$ and $g$ do not agree throughout their entire domain.
Thus:
:$\exists x \in S: \map f x \ne \map g x$
Then by definition of set union:
:$\exists S_k \subseteq S: x \in S_k$.
From the definition, both $f$ and $g$ are extensions of $S_k$.
But this means they must agree on $S_k$.
That is:
:$\forall x \in S_k: \map f x = \map g x$
This contradicts the supposition that $\map f x \ne \map g x$.
Thus:
:$\forall x \in S: \map f x = \map g x$
and $f$ has been shown to equal $g$.
Hence the result.
{{qed}}
Theorem: Futurama Theorem

Let $A_{n - 2} \subset A_n$ be a subgroup of the alternating group on $n$ letters $A_n$.
For any element $x \in A_{n - 2}$, let $x = x_1 x_2 \dots x_k$, where $x_i \in H$ is a transposition.
{{explain|What is $H$?}}
Then there exists $y$ which can be represented as a series of transpositions $y_1 y_2 \dots y_j \in A_n$ such that:
:$(1): \quad y x = z$, where $z$ contains no transpositions from $H$
:$(2): \quad y_a \ne x_b$ for all $a, b$.

Proof:
Let $w = (n [n - 1])$, that is, the transposition of the $n^{th}$ and $n - 1^{th}$ letters that we consider $A_n$ acting on.
Then the permutation $x^{-1} w$ is the $y$ of the theorem.
{{qed}}
Theorem: Pointwise Addition on Continuous Real Functions forms Group

Let $C$ be the set of all continuous real functions on the set of real numbers $\R$.
Let $f, g \in C$.
Let $f + g$ be the pointwise sum of $f$ and $g$:
:$\forall x \in R: \map {\paren {f + g} } x = \map f x + \map g x$
Then $\struct {C, +}$, the algebraic structure on $C$ induced by $+$, forms a group.

Proof:
Taking the group axioms in turn:
Theorem: General Intersection Property of Topological Space

Let $\struct {S, \tau}$ be a topological space.
Let $S_1, S_2, \ldots, S_n$ be open sets of $\struct {S, \tau}$.
Then:
:$\ds \bigcap_{i \mathop = 1}^n S_i$
is also an open set of $\struct {S, \tau}$.
That is, the intersection of any finite number of open sets of a topology is also in $\tau$.
Conversely, if the intersection of any finite number of open sets of a topology is also in $\tau$, then:
:$(1): \quad$ The intersection of any two elements of $\tau$ is an element of $\tau$
:$(2): \quad S$ is itself an element of $\tau$.

Proof:
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:For any sets $S_1, S_2, \ldots, S_n \in \tau$, it follows that $\ds \bigcap_{i \mathop = 1}^n S_i \in \tau$.
Let $\mathbb S$ be any finite subset of $\tau$.
From Intersection of Empty Set, we have that:
:$\mathbb S = \O \implies \bigcap \mathbb S = S$
From the definition of a topology, we have that $S \in \tau$.
Hence $\map P 0$ is true.
From Intersection of Singleton, we have that:
:$\mathbb S = S_1 \implies \bigcap \mathbb S = S_1$
Thus $\map P 1$ is trivially true.
Theorem: Empty Set is Element of Topology

Let $T = \struct {X, \tau}$ be a topological space.
Then the empty set $\O$ is an open set of $T$.

Proof:
By Empty Set is Subset of All Sets:
:$\O \subseteq \tau$
By Union of Empty Set:
:$\O = \bigcup \O$
By {{Open-set-axiom|1}}:
:$\O \in \tau$
{{qed}}
Category:Topology
Category:Empty Set
6b0ibvhzp9mr16tg9angho7kn8cv958
Theorem: Coarseness Relation on Topologies is Partial Ordering

Let $S$ be a set.
Let $\mathbb T$ be the set of all topologies on $S$.
Let $\le$ be the relation on $\mathbb T$ defined as:
:$\forall \tau_1, \tau_2 \in \mathbb T: \tau_1 \le \tau_2$ {{iff}} $\tau_1$ is coarser than $\tau_2$.
Then $\le$ is a partial ordering on $\mathbb T$.

Proof:
It follows directly from the definition of being coarser that:
:$\tau_1 \le \tau_2 \iff \tau_1 \subseteq \tau_2$
By Subset Relation is Ordering it thus follows that $\le$ is an ordering.
From Topologies are not necessarily Comparable by Coarseness, it follows that such an ordering is not always total.
{{qed}}
Theorem: Topology Defined by Closed Sets

Let $S$ be a set.
Let $\tau$ be a set of subsets of $S$.
Then $\tau$ is a topology on $S$ {{iff}}:
:$(1): \quad$ Any intersection of arbitrarily many closed sets of $S$ under $\tau$ is a closed set of $S$ under $\tau$
:$(2): \quad$ The union of any finite number of closed sets of $S$ under $\tau$ is a closed set of $S$ under $\tau$
:$(3): \quad S$ and $\O$ are both closed sets of $S$ under $\tau$
where a closed set $V$ of $S$ under $\tau$ is defined as a subset of $S$ such that $S \setminus V \in \tau$.

Proof:
From the definition, if $V$ is a closed set of $S$, then $S \setminus V$ is an open set of $S$.
Let $\mathbb V$ be any arbitrary set of closed sets of $S$.
Then by De Morgan's Laws: Difference with Intersection, we have:
:$\ds S \setminus \bigcap \mathbb V = \bigcup_{V \mathop \in \mathbb V} \paren {S \setminus V}$
First, let $\tau$ be a topology on $S$.
We have that:
:Intersection of Closed Sets is Closed in Topological Space
:Finite Union of Closed Sets is Closed in Topological Space
:By Open and Closed Sets in Topological Space, $\O$ and $S$ are both closed in $S$.
Thus, the properties as listed above hold.
{{qed|lemma}}
Suppose the properties:
:$(1): \quad$ Any intersection of arbitrarily many closed sets of $S$ under $\tau$ is a closed set of $S$ under $\tau$
:$(2): \quad$ The union of any finite number of closed sets of $S$ under $\tau$ is a closed set of $S$ under $\tau$
:$(3): \quad S$ and $\O$ are both closed sets of $S$ under $\tau$.
all hold.
That means $\ds \bigcap \mathbb V$ is closed.
So $\ds S \setminus \bigcap \mathbb V = \bigcup_{V \mathop \in \mathbb V} \paren {S \setminus V}$ is open.
Thus we have that the union of arbitrarily many open sets of $S$ under $\tau$ is an open set of $S$ under $\tau$.
Similarly, we deduce that the intersection of any finite number of open sets of $S$ under $\tau$ is an open set of $S$ under $\tau$.
By Open and Closed Sets in Topological Space, $\O$ and $S$ are both open in $S$.
So $\tau$ is a topology on $S$.
{{qed}}
Theorem: Complement of F-Sigma Set is G-Delta Set

Let $T = \struct {S, \tau}$ be a topological space.
Let $X$ be an $F_\sigma$ set of $T$.
Then its complement $S \setminus X$ is a $G_\delta$ set of $S$.

Proof:
Let $X$ be an $F_\sigma$ set of $T$.
Then $X = \ds \bigcup \VV$ where $\VV$ is a countable set of closed sets in $T$.
Then from De Morgan's Laws: Difference with Union we have:
:$\ds S \setminus X = S \setminus \bigcup \VV = \bigcap_{V \mathop \in \VV} \paren {S \setminus V}$
By definition of closed set, each of the $S \setminus V$ are open sets.
So $\ds \bigcap_{V \mathop \in \VV} \paren {S \setminus V}$ is a countable intersection of open sets in $T$.
Hence $S \setminus X$ is, by definition, a $G_\delta$ set of $T$.
{{qed}}
Theorem: Closed Set is F-Sigma Set

Let $T = \struct {S, \tau}$ be a topological space.
Let $V$ be a closed set of $T$.
Then $V$ is an $F_\sigma$ set of $T$.

Proof:
$V$ is the union of a singleton.
So $V$ is trivially the union of a countable number of closed sets of $T$.
The result follows by definition of $F_\sigma$ set.
{{qed}}
Theorem: Open Set is G-Delta Set

Let $T = \struct {S, \tau}$ be a topological space.
Let $U$ be an open set of $T$.
Then $U$ is a $G_\delta$ set of $T$.

Proof:
$U$ is the intersection of a singleton.
So $U$ is trivially the intersection of a countable number of open sets of $T$.
The result follows by definition of $G_\delta$ set.
{{qed}}
Theorem: Set is Open iff Neighborhood of all its Points

Let $T = \struct {S, \tau}$ be a topological space.
Let $V \subseteq S$ be a subset of $T$.
Then:
:$V$ is an open set of $T$
{{iff}}:
:$V$ is a neighborhood of all the points in $V$.

Proof:
=== Necessary Condition ===
Let $V$ be open in $T$.
Let $z \in V$.
By definition, a neighborhood of $z$ is any subset of $S$ containing an open set which itself contains $z$.
But $V$ is itself an open set which itself contains $z$.
Hence by Set is Subset of Itself, $V$ is a subset of $S$ which contains an open set which itself contains $z$.
So for all points of $z \in V$, $V$ is a neighborhood of $z$.
{{qed|lemma}}
Theorem: Relationship between Limit Point Types

Let $T = \struct {X, \tau}$ be a topological space.
Let $A \subseteq X$.
Let:
:$C$ be the set of condensation points of $A$
:$W$ be the set of $\omega$-accumulation points of $A$
:$L$ be the set of limit points of $A$
:$D$ be the set of adherent points of $A$.
Then:
:$C \subseteq W \subseteq L \subseteq D$
That is:
:Every condensation point is an $\omega$-accumulation point
:Every $\omega$-accumulation point is a limit point
:Every limit point is an adherent point.
In general, the inclusions do not hold in the other direction.

Proof:
Let $x \in C$.
By definition of condensation point, every open set of $T$ containing $x$ also contains an uncountable number of points of $A$.
As an uncountable number is also an infinite number, we could also say that every open set of $T$ containing $x$ also contains an infinite number of points of $A$.
That is, $x$ is also by definition an $\omega$-accumulation point.
So $x \in W$ and by definition of subset:
:$C \subseteq W$
Note that if $x \in W$ then it could be that there exists an open set $U$ of $T$ containing $x$ with a countably infinite number of points of $A$.
In that case $x \notin C$.
That is, not every $\omega$-accumulation point is necessarily a condensation point.
{{qed|lemma}}
Let $x \in W$.
By definition of $\omega$-accumulation point, every open set $U$ of $T$ containing $x$ also contains an infinite number of points of $A$.
So every open set $U$ of $T$ such that $x \in U$ contains some point of $A$ other than $x$ (an infinite number, indeed).
That is, $x$ is also by definition a limit point.
So $x \in L$ and by definition of subset:
:$W \subseteq L$
<!--
Note that if $x \in L$ then it could be that there exists an open set $U$ of $T$ containing $x$ which contains only a finite number of points of $A$.
In that case $x \notin W$.
-->
Let $T = \struct {S, \tau_p}$ be a particular point space.
From Limit Points in Particular Point Space, every point $x \ne p$ is a limit point of $T$.
From Point in Open Set of Particular Point Space is not Omega-Accumulation Point, $x$ is not an definition of $\omega$-accumulation point of $T$. 
So it is seen that not every limit point is necessarily an $\omega$-accumulation point.
{{qed|lemma}}
Let $x \in L$.
By definition of limit point, every open set $U$ of $T$ containing $x$ also contains some point of $A$ other than $x$.
So every open set $U$ of $T$ such that $x \in U$ contains some point of $A$.
That is, $x$ is also by definition an adherent point.
So $x \in L$ and by definition of subset:
:$L \subseteq D$
Note that if $x \in D$ then it could be that there exists an open set $U$ of $T$ containing $x$ in which the only point of $A$ is $x$ itself.
In that case $x \notin L$.
That is, not every adherent point is necessarily a limit point.
{{qed|lemma}}
Hence the result.
{{qed}}
Theorem: Limit of Sequence is Accumulation Point

Let $T = \struct {S, \tau}$ be a topological space.
Let $A \subseteq S$.
Let $\sequence {x_n}$ be a sequence in $A$.
Let $\alpha$ be a limit of $\sequence {x_n}$.
Then $\alpha$ is also an accumulation point of $\sequence {x_n}$.

Proof:
Let $\alpha$ be a limit of $\sequence {x_n}$.
Then by definition of limit, $\sequence {x_n}$ converges to $\alpha$.
By definition of convergence that means:
:for any open set $U \subseteq T$ such that $\alpha \in U$: $\exists N \in \R: n > N \implies x_n \in U$.
As there is an infinite number of values of $n > N$, there are an infinite number of terms of $\sequence {x_n}$.
Hence the result, from definition of accumulation point.
{{qed}}
Theorem: Sum of Independent Poisson Random Variables is Poisson

Let $X$ and $Y$ be independent discrete random variables with:
:$X \sim \Poisson {\lambda_1}$
and
:$Y \sim \Poisson {\lambda_2}$
for some $\lambda_1, \lambda_2 \in \R_{> 0}$.
Then their sum $X + Y$ is distributed:
:$X + Y \sim \Poisson {\lambda_1 + \lambda_2}$

Proof:
From Moment Generating Function of Poisson Distribution, the moment generating functions $X$ and $Y$, $M_X$ and $M_Y$, are given by: 
:$\map {M_X} t = e^{\lambda_1 \paren {e^t - 1} }$
and
:$\map {M_Y} t = e^{\lambda_2 \paren {e^t - 1} }$
As $X$ and $Y$ are independent, we may apply Moment Generating Function of Linear Combination of Independent Random Variables, to give: 
{{begin-eqn}}
{{eqn	| l = \map {M_{X + Y} } t 
	| r = \map {M_X} t \map {M_Y} t
	| c = Moment Generating Function of Linear Combination of Independent Random Variables
}}
{{eqn	| r = e^{\lambda_1 \paren {e^t - 1} } e^{\lambda_2 \paren {e^t - 1} }
}}
{{eqn	| r = e^{\paren {\lambda_1 + \lambda_2} \paren {e^t - 1} }
	| c = Exponential of Sum
}}
{{end-eqn}}
This is the moment generating function of a random variable with distribution $\Poisson {\lambda_1 + \lambda_2}$. 
So, $X + Y \sim \Poisson {\lambda_1 + \lambda_2}$.
{{qed}}
Theorem: Filter on Set is Proper Filter

Let $S$ be a set.
Let $\powerset S$ denote the power set of $S$.
Let $\struct {\powerset S, \subseteq}$ be the poset defined on $\powerset S$ by the subset relation.
Let $\FF$ be a filter on $S$.
Then $\FF$ is a proper filter on $\struct {\powerset S, \subseteq}$.

Proof:
From the general definition of a filter, we have:
A '''filter on $\struct {S, \preccurlyeq}$''' is a subset $\FF \subseteq S$ which satisfies the following conditions:
:$\FF \ne \O$
:$x, y \in \FF \implies \exists z \in \FF: z \preccurlyeq x, z \preccurlyeq y$
:$\forall x \in \FF: \forall y \in S: x \preccurlyeq y \implies y \in \FF$
A filter $\FF$ is proper if it does not equal $S$ itself.
From the definition of a filter on a set, we have:
A '''filter on $T$''' is a set $\FF \subset \powerset T$ which satisfies the following conditions:
:$T \in \FF$
:$\O \notin \FF$
:$U, V \in \FF \implies U \cap V \in \FF$
:$\forall U \in \FF: U \subseteq V \subseteq T \implies V \in \FF$
We can identify:
:$\powerset T$ with $S$
:$\subseteq$ with $\preccurlyeq$.
Theorem: Peirce's Law is Equivalent to Law of Excluded Middle

Peirce's Law:
:$\paren {p \implies q} \implies p \vdash p$
is logically equivalent to the Law of Excluded Middle:
:$\vdash p \lor \neg p$
That is, Peirce's Law holds {{iff}} the Law of Excluded Middle holds.

Proof:
=== Law of Excluded Middle implies Peirce's Law ===
{{:Law of Excluded Middle implies Peirce's Law}}
{{qed|lemma}}
Theorem: Conditional is Left Distributive over Conjunction

The implication operator is left distributive over the conjunction operator:
=== Formulation 1 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 2}}

Proof:
{{BeginTableau|p \implies \paren {q \land r} \vdash \paren {p \implies q} \land \paren {p \implies r} }}
{{Premise|1|p \implies \paren {q \land r} }}
{{Assumption|2|p}}
{{ModusPonens|3|1, 2|q \land r|1|2}}
{{Simplification|4|1, 2|q|3|1}}
{{Simplification|5|1, 2|r|3|2}}
{{Implication|6|1|p \implies q|2|4}}
{{Implication|7|1|p \implies r|2|5}}
{{Conjunction|8|1|\paren {p \implies q} \land \paren {p \implies r}|6|7}}
{{EndTableau|qed}}
Theorem: Conditional is Left Distributive over Conjunction

The implication operator is left distributive over the conjunction operator:
=== Formulation 1 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 2}}

Proof:
=== Proof of Forward Implication ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1/Forward Implication/Proof}}
=== Proof of Reverse Implication ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1/Reverse Implication/Proof}}
Theorem: Conditional is Left Distributive over Conjunction

The implication operator is left distributive over the conjunction operator:
=== Formulation 1 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
p & \implies & (q & \land & r) & (p & \implies & q) & \land & (p & \implies & r) \\
\hline
\F & \T & \F & \F & \F & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \F & \T & \F & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \F & \T & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \F & \F & \T & \F & \F \\
\T & \F & \F & \F & \T & \T & \F & \F & \F & \T & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Conditional is Left Distributive over Conjunction

The implication operator is left distributive over the conjunction operator:
=== Formulation 1 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 2}}

Proof:
{{BeginTableau|\paren {p \implies q} \land \paren {p \implies r} \vdash p \implies \paren {q \land r} }}
{{Premise|1|\paren {p \implies q} \land \paren {p \implies r} }}
{{SequentIntro|2|1|\paren {p \land p} \implies \paren {q \land r}|1|Praeclarum Theorema}}
{{Assumption|3|p}}
{{Idempotence|4|3|p \land p|3|Conjunction}}
{{ModusPonens|5|1, 3|q \land r|2|4}}
{{Implication|6|1|p \implies \paren {q \land r}|3|5}}
{{EndTableau}}
{{qed}}
Theorem: Conditional is Left Distributive over Conjunction

The implication operator is left distributive over the conjunction operator:
=== Formulation 1 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 2}}

Proof:
Let us use the following abbreviations
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text {for}
      | r = p \implies \paren {q \land r}
      | c = 
}}
{{eqn | l = \psi
      | o = \text {for}
      | r = \paren {p \implies q} \land \paren {p \implies r}
      | c = 
}}
{{end-eqn}}
{{BeginTableau|\vdash \phi \implies \psi}}
{{Assumption|1|\phi}}
{{SequentIntro|2|1|\psi|1|Conditional is Left Distributive over Conjunction: Formulation 1}}
{{Implication|3||\phi \implies \psi|1|2}}
{{EndTableau}}
Expanding the abbreviations leads us back to:
:$\paren {p \implies \paren {q \land r} } \implies \paren {\paren {p \implies q} \land \paren {p \implies r} }$
{{qed}}
Theorem: Conditional is Left Distributive over Conjunction

The implication operator is left distributive over the conjunction operator:
=== Formulation 1 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 2}}

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

The implication operator is left distributive over the conjunction operator:
=== Formulation 1 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|ccccccc|} \hline
(p & \implies & (q & \land & r)) & \iff & ((p & \implies & q) & \land & (p & \implies & r)) \\
\hline
\F & \T & \F & \F & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \F & \T & \T & \F & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \T & \F & \T & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \F & \T & \T & \F & \F & \F & \T & \F & \F \\
\T & \F & \F & \F & \T & \T & \T & \F & \F & \F & \T & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}