avewright/proofwiki-math huggingface dataset:
Theorem: Tableau Confutation is Finished

Let $T$ be a tableau confutation.
Then $T$ is a finished tableau.

Proof:
By definition of tableau confutation, every branch of $T$ is contradictory.
The result follows by definition of finished propositional tableau.
{{qed}}
Theorem: Expression of Vector as Linear Combination from Basis is Unique/General Result

Let $V$ be a vector space over a division ring $R$.
Let $B$ be a basis for $V$.
Let $x \in V$.
Then there is a unique finite subset $C$ of $R \times B$ such that:
:$\ds x = \sum_{\tuple {r, v} \mathop \in C} r \cdot v$
:$\forall \tuple {r, v} \in C: r \ne 0_R$

Proof:
=== Existence ===
The existence of $C$ follows immediately from the definition of a basis.
{{qed|lemma}}
Theorem: Dependent Choice for Finite Sets

Let $\RR$ be a binary relation on a non-empty set $S$.
For each $a \in S$, let $C_a = \set {b \in S: a \mathrel \RR b }$
Suppose that:
:For all $a \in S$, $C_a$ is a non-empty finite set.
Let $s \in S$.
Then there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $S$ such that:
:$x_0 = s$
:$\forall n \in \N: x_n \mathrel \RR x_{n+1}$

Proof:
Define $\sequence {D_n}$ recursively:
Let $D_0 = \set s$.
For each $n \in \N$ let $D_{n + 1} = \map \RR {D_n}$.
Now, for each $n \in \N$ let $E_n$ be the set of all enumerations of $D_n$.
Then $E_n$ is non-empty and finite for each $n$.
By the Axiom of Countable Choice for Finite Sets, there is a sequence $\sequence {e_n}$ such that for each $n$, $e_n \in E_n$.
Now recursively define $\sequence {x_n}$:
:Define $x_0$ as $s$.
:Define $x_{n + 1}$ as the first element in the enumeration $e_n$ which is in $\map \RR {x_n}$.
Then $\sequence {x_n}$ is the required sequence.
{{qed}}
{{Choice-principle|Axiom:Axiom of Countable Choice for Finite Sets}}
Theorem: Dependent Choice (Fixed First Element)

Let $\RR$ be a binary relation on a non-empty set $S$.
Suppose:
:$\forall a \in S: \exists b \in S: a \mathrel \RR b$
that is, that $\RR$ is a left-total relation (that is, a serial relation).
Let $s \in S$.
Then there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $S$ such that:
:$x_0 = s$
:$\forall n \in \N: x_n \mathrel \RR x_{n + 1}$

Proof:
Let $S' = \set {y \in S: s \mathrel {\RR^+} y}$, where $\RR^+$ is the transitive closure of $\RR$.
Let $\RR'$ be the restriction of $\RR$ to $S'$. 
For each $x \in S'$, there is a $y \in S$ such that $x \mathrel \RR y$. But then $s \mathrel {\RR^+} y$, so $y \in S'$, so $x \mathrel {\RR'} y$.
Thus $\RR'$ is a left-total relation on $S'$.
$S'$ is non-empty: since $\RR$ is left-total, there is a $t \in S$ such that $s \mathrel \RR t$, so $s \mathrel {\RR^+} t$, so $t \in S'$.
By Axiom of Dependent Choice, there is a infinite sequence $\sequence {y_n}_{n \mathop \in \N}$ in $S'$ such that for each $n \in \N$, $y_n \mathrel {\RR'} y_{n + 1}$.
Then by definition of restriction, $y_n \mathrel \RR y_{n + 1}$ for each $n \in \N$.
By definition of $S'$, $s \mathrel {\RR^+} y_0$.
By definition of transitive closure, there are elements $x_0, \dots, x_m$ such that $s = x_0 \mathrel \RR x_1 \mathrel \RR \cdots \mathrel \RR x_m \mathrel \RR x_m = y_0$.
Then for $n > m$, define $x_n$ as $y_{n - m}$.
This sequence then meets the requirements.
{{qed}}
{{ADC}}
Category:Set Theory
phtyq1rpaa6kfs9l6rjesrrxlofw9fa
Theorem: Locally Finite Connected Graph is Countable

Let $G = \struct {V, E}$ be a graph which is connected and locally finite.
Then $G$ has countably many vertices and countably many edges.

Proof:
We first show that $V$ is countable.
If $V$ is finite, then it is surely countable.
Suppose instead that $V$ is infinite.
Choose an arbitrary vertex $q \in V$.
Recursively define a sequence $\sequence {S_n}$:
:Let $S_0 = \set q$.
:Let $S_{n + 1}$ be the set of all vertices that are adjacent to some element of $S_n$ but ''not'' adjacent to any element of $S_k$ for $k < n$.
:That is, $S_n$ is the set of vertices whose shortest path(s) to $q$ have $n$ edges.
Since $G$ is connected, $V = \ds \bigcup_{n \mathop \in \N} S_n$.
{{explain|Trivial, but requires talking about walks and all.}}
Furthermore, $S_n$ is finite and non-empty for each $n$.
{{explain}}
But by Countable Union of Finite Sets is Countable, $\ds \bigcup_{n \mathop \in \N} S_n$ is countable, so $V$ is countable.
{{ExtractTheorem|Set of Unordered Pairs of Countable Set is Countable or some such.}}
By Cartesian Product of Countable Sets is Countable, $V \times V$ is countable.
Let $E' = \set {\tuple {a, b}: \set {a, b} \in E}$.
By Subset of Countable Set is Countable, $E'$ is countable.
Let $g: E' \to E$ be defined by $\map g {a, b} = \set {a, b}$.
Then $g$ is surjective.
Thus by Surjection from Natural Numbers iff Countable and Composite of Surjections is Surjection, $E$ is countable as well.
{{qed}}
{{Choice-principle|Axiom:Axiom of Countable Choice for Finite Sets|Countable Union of Finite Sets is Countable}}
Category:Graph Theory
sy6dqvlw7seoqqjmvom491ieqn2z9pa
Theorem: Law of Cosines/Right Triangle

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that:
: $a$ is opposite $A$
: $b$ is opposite $B$
: $c$ is opposite $C$.
Let $\triangle ABC$ be a right triangle such that $\angle A$ is right.
Then:
:$c^2 = a^2 + b^2 - 2 a b \cos C$

Proof:
Let $\triangle ABC$ be a right triangle such that $\angle A$ is right.
:300px
{{begin-eqn}}
{{eqn | l = a^2
      | r = b^2 + c^2
      | c = Pythagoras's Theorem
}}
{{eqn | l = c^2
      | r = a^2 - b^2
      | c = adding $-b^2$ to both sides and rearranging
}}
{{eqn | r = a^2 - 2 b^2 + b^2
      | c = adding $0 = b^2 - b^2$ to the {{RHS}}
}}
{{eqn | r = a^2 - 2 a b \left({\frac b a}\right) + b^2
      | c = multiplying $2 b^2$ by $\dfrac a a$
}}
{{eqn | r = a^2 + b^2 - 2 a b \cos C
      | c = {{Defof|Cosine of Angle|Cosine}}: $\cos C = \dfrac b a$
}}
{{end-eqn}}
Theorem: Minimally Inductive Set is Minimal

The minimally inductive set $\omega$ is a subset of every inductive set.

Proof:
Let $A$ be an inductive set.
Let $B$ be another arbitrary inductive set.
Then from Intersection is Subset, $A \cap B \subseteq A$.
From Intersection of Inductive Sets, $A \cap B$ is also an inductive set.
This set $A \cap B$ is one of the subsets
By the definition of $\omega$ it follows that $\omega \subseteq A \cap B$, and consequently that $\omega \subseteq B$.
{{qed}}
Theorem: Law of Cosines/Proof 3/Acute Triangle

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that:
:$a$ is opposite $A$
:$b$ is opposite $B$
:$c$ is opposite $C$.
Let $\triangle ABC$ be an acute triangle.
Then:
:$c^2 = a^2 + b^2 - 2a b \cos C$

Proof:
Let $\triangle ABC$ be an acute triangle.
:300px
Let $BD$ be dropped perpendicular to $AC$.
Let:
{{begin-eqn}}
{{eqn | l = h
      | r = BD
}}
{{eqn | l = e
      | r = CD
}}
{{eqn | l = f
      | r = AD
}}
{{end-eqn}}
We have that $\triangle CDB$ and $\triangle ADB$ are right triangles.
Hence:
{{begin-eqn}}
{{eqn | n = 1
      | l = c^2
      | r = h^2 + f^2
      | c = Pythagoras's Theorem
}}
{{eqn | n = 2
      | l = a^2
      | r = h^2 + e^2
      | c = Pythagoras's Theorem
}}
{{eqn | n = 3
      | l = b^2
      | r = \paren {e + f}^2
      | c = 
}}
{{eqn | r = e^2 + f^2 + 2ef
      | c = 
}}
{{eqn | n = 4
      | l = e
      | r = a \cos C
      | c = {{Defof|Cosine of Angle}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = c^2 
      | r = h^2 + f^2
      | c = from $(1)$
}}
{{eqn | r = a^2 - e^2 + f^2
      | c = from $(2)$
}}
{{eqn | r = a^2 - e^2 + f^2 + 2 e^2 - 2 e^2 + 2 e f - 2 e f
      | c = adding and subtracting $2 e^2$ and $2 e f$
}}
{{eqn | r = a^2 + \paren {e^2 + f^2 + 2 e f} - 2 e \paren {e + f}
      | c = rearanging
}}
{{eqn | r = a^2 + b^2 - 2 a b \cos C
      | c = using $(3)$ to substitute for $b^2$ and $b$, and $(4)$ to substitute $e$ for $a \cos C$
}}
{{end-eqn}}
Theorem: Law of Cosines/Proof 3/Obtuse Triangle

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that:
: $a$ is opposite $A$
: $b$ is opposite $B$
: $c$ is opposite $C$.
Let $\triangle ABC$ be an obtuse triangle such that $A$ is obtuse
Then:
:$c^2 = a^2 + b^2 - 2a b \cos C$

Proof:
Let $\triangle ABC$ be an obtuse triangle.
:300px
Let $AC$ be extended and $BD$ be dropped perpendicular to $AC$.
Let:
{{begin-eqn}}
{{eqn | l = h
      | r = BD
}}
{{eqn | l = e
      | r = CD
}}
{{eqn | l = f
      | r = AD
}}
{{end-eqn}}
We have that $\triangle CDB$ and $\triangle ADB$ are right triangles.
Hence:
{{begin-eqn}}
{{eqn | n = 1
      | l = c^2
      | r = h^2 + f^2
      | c = Pythagoras's Theorem
}}
{{eqn | n = 2
      | l = a^2
      | r = h^2 + e^2
      | c = Pythagoras's Theorem
}}
{{eqn | n = 3
      | l = e^2
      | r = \paren {b + f}^2
      | c = 
}}
{{eqn | r = b^2 + f^2 + 2 b f
      | c = 
}}
{{eqn | n = 4
      | l = e
      | r = a \cos C
      | c = {{Defof|Cosine of Angle}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = c^2 
      | r = h^2 + f^2
      | c = from $(1)$
}}
{{eqn | r = a^2 - e^2 + f^2
      | c = from $(2)$
}}
{{eqn | r = a^2 - b^2 - f^2 - 2 b f + f^2
      | c = substituting for $e^2$ from $(3)$
}}
{{eqn | r = a^2 - b^2 - 2 b f + 2 b^2 - 2 b^2
      | c = simplifying and adding and subtracting  $2 b^2$
}}
{{eqn | r = a^2 + b^2 - 2 b \paren {b + f}
      | c = rearranging
}}
{{eqn | r = a^2 + b^2 - 2 a b \cos C
      | c = using $(4)$ to substitute $b + f = e$ with $a \cos C$
}}
{{end-eqn}}
Theorem: König's Lemma/Countable

Let $G = \struct {V, E}$ be a graph with countably infinitely many vertices which is connected and is locally finite.
Then every vertex of $G$ lies on a path of infinite length.

Proof:
Let $r$ be a vertex of $G$.
Recursively define a sequence $\sequence {S_n}$:
Let $S_0 = \set r$.
Let $S_{n + 1}$ be the set of all vertices that are adjacent to some element of $S_n$ but ''not'' adjacent to any element of $S_k$ for $k < n$.
That is, $S_n$ is the set of vertices whose shortest path(s) to $r$ have $n$ edges.
Since $G$ is connected:
:$\ds V = \bigcup_{n \mathop \in \N} S_n$
Note that $\set {S_n: n \in \N}$ is pairwise disjoint.
Define a relation $\RR$ on $V$ by letting $p \mathrel \RR q$ {{iff}}:
:$p$ is adjacent to $q$
and:
:there exists an $n \in \N$ such that $p \in S_n$ and $q \in S_{n + 1}$.
Let $\RR^+$ be the transitive closure of $\RR$.
Let $V'$ be the set of all $v \in V$ such that $\map {\RR^+} v$ is infinite.
It will be demonstrated that $r \in V'$:
Let $v \in V$.
Since $G$ is connected, there is a path from $r$ to $v$.
By the Well-Ordering Principle, there is a path $P$ from $r$ to $v$ of minimal length.
Then the vertices along $P$ will lie in successive sets $S_k$.
{{explain}}
Thus $v \in \map {\RR^+} r$.
As this holds for all $v \in V$, and $V$ is infinite, $\map {\RR^+} r$ is infinite.
Therefore $r \in V'$.
Let $\RR'$ be the restriction of $\RR$ to $V'$.
It is to be shown that $\RR'$ is a left-total relation.
Let $v \in V'$.
Then $\map {\RR^+} v$ is infinite.
Since $\map \RR v$ is finite, Finite Union of Finite Sets is Finite shows that $\map \RR v$ must have an element $u$ such that $\map {\RR^+} u$ is infinite.
So $u \in V'$ and $v \mathrel {\RR'} u$.
We have that $V$ is assumed to be countably infinite.
{{WLOG}}, let $V = \N$.
Recursively define a sequence $\sequence {v_k}$ in $V'$ thus:
:$v_0 = r$
:$v_{n + 1} = \map \min {\map {\RR'} {v_n} }$
Then $\sequence {v_k}$ is the sequence of vertices along an infinite path starting at $r$.
{{qed}}
{{Namedfor|Dénes Kőnig}}
Category:König's Lemma
754durtrk4hrn6mcrc2qj0jb7st4y2u
Theorem: Paths of Minimal Length from Vertex form Tree

Let $G = \struct {V, E}$ be a simple graph.
Let $r \in V$ be a vertex in $G$.
Let $P$ be the set of minimal length paths beginning at $r$.
Let $p, q \in P$.
Let $E'$ be defined as follows:
$\set {p, q} \in E'$ {{iff}} either:
:$q$ is formed by extending $p$ with one edge of $E$ and one vertex of $V$
or:
:$p$ is formed by extending $q$ with one edge of $E$ and one vertex of $V$.
Then $T = \struct {P, E'}$ is a tree.

Proof:
Let $\tuple r$ be the $0$-length $G$-path whose only vertex is $r$.
Theorem: Finite Sequences in Set Form Acyclic Graph

Let $S$ be a set.
Let $V$ be the set of finite sequences in $S$.
Let $E$ be the set of unordered pairs $\set {p, q}$ of elements of $V$ such that either:
:$q$ is formed by extending $p$ by one element or
:$p$ is formed by extending $q$ by one element.
That is:
:$\card {\Dom p \symdif \Dom q} = 1$, where $\symdif$ is symmetric difference
:$p \restriction D = q \restriction D$, where $D = \Dom p \cap \Dom q$
Then $T = \struct{V, E}$ is an acyclic graph.

Proof:
{{proof wanted}}
Category:Graph Theory
ttrxo7lcehixqwf34y9hf4oiyifowb6
Theorem: Four Color Theorem for Finite Maps implies Four Color Theorem for Infinite Maps

Suppose that any finite planar graph can be assigned a proper vertex $k$-coloring such that $k \le 4$.
Then the same is true of any infinite planar graph.

Proof:
Let $G$ be an infinite planar graph.
Let $C$ be a set of vertices of $G$.
For each $c \in C$ let $p_c^1, p_c^2, p_c^3, p_c^4$ be propositional symbols, where
: $p_c^i$ is true {{iff}} the color of vertex $c$ is $i$.
Let $\PP_0$ be the vocabulary defined as:
:$\PP_0 = \set {p_c^1, p_c^2, p_c^3, p_c^4: c \in C}$
Let $\mathbf H$ be the set of all statements with the following forms:
:$(1): \quad$ $p_c^1 \lor p_c^2 \lor p_c^3 \lor p_c^4$ for each $c \in C$
:$(2): \quad$ $p_c^i \implies \neg p_c^j$ for each $c \in C$ and for each $i \ne j$
:$(3): \quad$ $\neg \paren {p_c^i \land \neg p_{c'}^i}$ for each $i$ where $c$ and $c'$ are adjacent.
Let $\MM$ be a model for $\mathbf H$ which corresponds to a proper vertex $4$-coloring of $G$.
By hypothesis, any finite planar graph can be assigned a proper vertex $4$-coloring.
Thus every finite subgraph of $G$ has a proper vertex $4$-coloring.
That is, every finite subset of $\mathbf H$ has a model.
By the Compactness Theorem for Boolean Interpretations, $\mathbf H$ has a model.
Hence the entirety of $G$ can be assigned a proper vertex $k$-coloring.
{{qed}}
Theorem: Connected Vertices are Connected by Path

Let $G = \struct {V, E}$ be a simple graph.
Let $x, y \in V$.
Let there exist a walk $w: \N_n \to V$ from $x$ to $y$.
Then there exists a subsequence $z_n$ of $w$ which is a path from $x$ to $y$.

Proof:
We represent a walk as a sequence of vertices.
However, the same argument will work for the representation as an alternating sequence of vertices and edges.
The proof proceeds by induction on the length of $w$.
If the length of $w$ is $0$, then it is trivially a path.
Suppose that every walk of length less than $n$ has a subsequence forming a path between its endpoints.
Let $w$ have length $n$.
If $w$ is not a path, then it must have a cycle.
That is, for some $j, k \in \Dom w$, $j < k$ and $w_j = w_k$.
Then removing $w_{j + 1}, \dots, w_k$ from $w$ will form a new walk $w'$, from $x$ to $y$ which is strictly shorter than $w$.
By the inductive hypothesis, $w'$ has as subsequence which is a path from $x$ to $y$.
{{qed}}
Category:Graph Theory
srv00yb34cr37uj72p3dzo2tsy6q17b
Theorem: Rooted Tree Corresponds to Arborescence

Let $T = \struct {V, E}$ be a rooted tree with root $r$.
Then there is a unique orientation of $T$ which is an $r$-arborescence.

Proof:
Recall that a tree is connected and has no cycles.
Thus there is exactly one path from each node of $T$ to each other node of $T$.
{{explain|This is in fact a result that already exists and can be quoted directly.}}
Let $A$ be the set of all ordered pairs $x, y \in V$ such that:
:$\tuple {x, y} \in E$ and
:The unique path from $r$ to $y$ passes through $x$.
{{finish}}
Theorem: Equivalence of Definitions of Arborescence

Let $G = \struct {V, A}$ be a digraph.
Let $r \in V$.
{{TFAE|def = Arborescence}}

Proof:
=== Definition 1 implies Definition 3 ===
Let $G$ be an $r$-arborescence by definition 1.
Let $v \in V$ such that $v \ne r$.
Then there is exactly one directed walk $w$ from $r$ to $v$.
Since $v \ne r$, either:
:$w = \tuple {r, v}$
or:
:$\exists m \in V: w = \tuple {r, \ldots, m, v}$
Thus $v$ is the final vertex of the arc $r v$ or the arc $m v$.
{{AimForCont}} that $v$ is the final vertex of distinct arc $x v$ and $y v$.
Then there exist directed walks $w_1$ and $w_2$ from $r$ to $x$ and $r$ to $y$ respectively.
But appending $v$ to $w_1$ and to $w_2$ yields distinct directed walks from $r$ to $v$.
This contradicts the fact that there is exactly one such directed walk.
Thus $v$ is the final vertex of exactly one arc.
{{qed|lemma}}
{{AimForCont}} that $r$ is the final vertex of an arc $x r$.
By Definition 1, there is a directed walk $w$ from $r$ to $x$.
But then $w$ appended to $w$ is a directed walk from $r$ to $x$ which is not equal to $w$.
This contradicts definition 1.
Thus we conclude that $r$ is not the final vertex of any arc.
It follows immediately from definition 1 that there is a directed walk from $r$ to each vertex $v \ne r$.
Thus $G$ is an $r$-arborescence by Definition 3.
{{qed|lemma}}
Theorem: Negation as Implication of Bottom

$p \implies \bot \dashv\vdash \neg p$

Proof:
{{BeginTableau|p \implies \bot \vdash \neg p}}
{{Premise|1|p \implies \bot}}
{{Assumption|2|p}}
{{ModusPonens|3|1,2|\bot|1|2}}
{{Contradiction|4|1|\neg p|2|3}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|\neg p \vdash p \implies \bot}}
{{Premise|1|\neg p}}
{{Assumption|2|p}}
{{NonContradiction|3|1,2|1|2}}
{{Implication|4|1|p \implies \bot|2|3}}
{{EndTableau}}
{{qed}}
neczwy8yehl9o1wbr73v4ga4vw7fe7e
Theorem: Clavius's Law implies Law of Excluded Middle

From Clavius's Law:
:$\neg p \implies p \vdash p$
follows the Law of Excluded Middle:
:$\vdash p \lor \neg p$

Proof:
{{BeginTableau|\vdash p \lor \neg p}}
{{Assumption|1|\neg (p \lor \neg p)}}
{{SequentIntro|2|1|\bot|1|Negation of Excluded Middle is False}}
{{Explosion|3|1|p \lor \neg p|2}}
{{Implication|4||\neg(p \lor \neg p) \implies p \lor \neg p|1|3}}
{{SequentIntro|5||p \lor \neg p|4|Clavius's Law}}
{{EndTableau}}
{{qed}}
Theorem: Parity of Integer equals Parity of its Square/Even

Let $p \in \Z$ be an integer.
Let $p$ be even.
Then $p^2$ is also even.

Proof:
Let $r = 0$, so:
:$p = 2 k$
Then:
:$p^2 = \paren {2 k}^2 = 4 k^2 = 2 \paren {2 k^2}$
and so $p^2$ is even.
Theorem: Parity of Integer equals Parity of its Square/Odd

Let $p \in \Z$ be an integer.
Let $p$ be odd.
Then $p^2$ is also odd.

Proof:
Let $r = 1$, so:
:$p = 2 k + 1$
Then:
:$p^2 = \paren {2 k + 1}^2 = 4 k^2 + 4 k + 1 = 2 \paren {2 k^2 + 2 k} + 1$
and so $p^2$ is odd.
Theorem: Negation of Excluded Middle is False/Form 1

$\neg (p \lor \neg p) \vdash \bot$

Proof:
{{BeginTableau|\neg (p \lor \neg p) \vdash \bot}}
{{Assumption|1|\neg (p \lor \neg p)}}
{{SequentIntro|2|1|\neg p \land \neg \neg p|1|De Morgan's Laws}}
{{Simplification|3|1|\neg p|2|1}}
{{Simplification|4|1|\neg\neg p|2|2}}
{{NonContradiction|5|1|3|4}}
{{EndTableau}}
{{qed}}
Theorem: Negation of Excluded Middle is False/Form 2

$\vdash \neg \neg (p \lor \neg p)$

Proof:
{{BeginTableau|\neg\neg (p \lor \neg p)}}
{{Assumption|1|\neg (p \lor \neg p)}}
{{SequentIntro|2|1|\bot|1|Negation of Excluded Middle is False: Form 1}}
{{Implication|3||\neg (p \lor \neg p) \implies \bot|1|2}}
{{SequentIntro|4||\neg \neg (p \lor \neg p)|3|Negation as Implication of Bottom}}
{{EndTableau}}
{{qed}}
Category:Propositional Logic
9inhesbm7f2swudqcr1zrzyh8j4zygg
Theorem: Injection iff Left Cancellable/Necessary Condition

Let $f: Y \to Z$ be an injection.
Then $f$ is left cancellable.

Proof:
Let $f: Y \to Z$ be an injection.
Let $X$ be a set
Let $g_1: X \to Y, g_2: X \to Y$ be mappings such that:
: $f \circ g_1 = f \circ g_2$
Then $\forall x \in X$:
{{begin-eqn}}
{{eqn | l = \map f {g_1 \paren x}
      | r = \map {f \circ g_1} x
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map {f \circ g_2} x
      | c = By Hypothesis
}}
{{eqn | r = \map f {\map {g_2} x}
      | c = {{Defof|Composite Mapping}}
}}
{{end-eqn}}
As $f$ is an injection, $\map {g_1} x = \map {g_2} x$ and thus the condition for left cancellability holds.
Theorem: Injection iff Left Cancellable/Sufficient Condition

Let $f: Y \to Z$ be a mapping which is left cancellable.
Then $f$ is an injection.

Proof:
We use a Proof by Contraposition.
That is, we show that if $f: Y \to Z$ is not injective, then $f$ is not left cancellable.
Hence, suppose $f: Y \to Z$ is not injective.
Then:
: $\exists y_1 \ne y_2 \in Y: f \left({y_1}\right) = f \left({y_2}\right)$
Let the two mappings $g_1: Y \to Y, g_2: Y \to Y$ be defined as follows:
:$\forall y \in Y: g_1 \left({y}\right) = y$
:$\forall y \in Y: g_2 \left({y}\right) = \begin{cases}
y_2 & : y = y_1 \\
y & : y \ne y_1
\end{cases}$
Thus we have $g_1 \ne g_2$ such that $f \circ g_1 = f \circ g_2$.
That is, $f$ is not left cancellable.
From Rule of Transposition it follows that if $f$ is left cancellable, it is injective.
Theorem: Peirce's Law implies Law of Excluded Middle

From Peirce's Law:
:$\paren {p \implies q} \implies p \vdash p$
follows the Law of Excluded Middle:
:$\vdash p \lor \neg p$

Proof:
{{BeginTableau|\vdash p \lor \neg p}}
{{Assumption|1|\paren {p \lor \neg p} \implies \bot}}
{{SequentIntro|2|1|\neg \paren {p \lor \neg p}|1|Negation as Implication of Bottom}}
{{SequentIntro|3|1|\bot|2|Negation of Excluded Middle is False}}
{{Explosion|4|1|p \lor \neg p|3}}
{{Implication|5||\paren {\paren {p \lor \neg p} \implies \bot} \implies p \lor \neg p|1|4}}
{{SequentIntro|6||p \lor \neg p|5|Peirce's Law: $p \gets p \lor \neg p$, $q \gets \bot$}}
{{EndTableau}}
{{qed}}
Theorem: Pseudocomplemented Lattice is Bounded

Let $\struct {L, \wedge, \vee, \preceq}$ be a pseudocomplemented lattice.
Then $\struct {L, \wedge, \vee, \preceq}$ is a bounded lattice.

Proof:
By the definition of pseudocomplemented lattice, $L$ has a smallest element $\bot$.
Let $x \in L$.
Then:
:$x \wedge \bot = \bot$
{{explain}}
By the definition of pseudocomplemented lattice, there is a greatest element $\bot^*$ such that:
:$\bot \wedge \bot^* = \bot$
But then by the definition of greatest element:
:$\forall x \in L: x \preceq \bot^*$
Hnce.o $\bot^*$ is the greatest element of $L$.
Since $L$ has a smallest element and a greatest element, it is a bounded lattice.
{{qed}}
Category:Pseudocomplemented Lattices
Category:Bounded Lattices
i2pj1o1x1bref9yh37sz5va2m51yjmp
Theorem: Topology forms Complete Lattice

Let $\struct {X, \tau}$ be a topological space.
Then $\struct {\tau, \subseteq}$ is a complete lattice.

Proof:
To show that $\struct {\tau, \subseteq}$ is a complete lattice, we must show that every subset of $\tau$ has a supremum and an infimum.
Let $S \subseteq \tau$.
By the definition of a topology:
:$\ds \bigcup S \in \tau$
By Union is Smallest Superset, $\ds \bigcup S$ is the supremum of $S$.
Let $I$ be the interior of $\ds \bigcap S$, where by Intersection of Empty Set $\ds \bigcap \O$ is conventionally taken to be $X$.
Then by the definition of interior and Intersection is Largest Subset:
:$I \in \tau$
and
:$I \subseteq U$
for each $U \in S$.
Let $V \in \tau$ with $V \subseteq U$ for each $U \in S$.
By Intersection is Largest Subset:
:$\ds V \subseteq \bigcap S$.
Then by the definition of interior:
:$V \subseteq I$
Thus $I$ is the infimum of $S$.
So each subset of $\tau$ has a supremum and an infimum.
Thus, by definition, $\struct {\tau, \subseteq}$ is a complete lattice.
{{qed}}
Category:Topology
Category:Complete Lattices
50c7zlvv6w4sz001wn3hfxrzg4y6gxo
Theorem: Law of Excluded Middle implies Peirce's Law

From the Law of Excluded Middle follows Peirce's Law:
:$\paren {p \lor \neg p} \vdash \paren {\paren {p \implies q} \implies p} \implies p$

Proof:
{{BeginTableau|\paren {p \lor \neg p} \vdash \paren {\paren {p \implies q} \implies p} \implies p}}
{{Premise|1|p \lor \neg p}}
{{Assumption|2|p}}
{{SequentIntro|3|2|\paren {\paren {p \implies q} \implies p} \implies p|2|True Statement is implied by Every Statement}}
{{Assumption|4|\neg p}}
{{SequentIntro|5|4|p \implies q|4|False Statement implies Every Statement}}
{{Assumption|6|\paren {p \implies q} \implies p}}
{{ModusPonens|7|4, 6|p|6|5}}
{{Implication|8|4|\paren {\paren {p \implies q} \implies p} \implies p|6|7}}
{{ProofByCases|9|1|\paren {\paren {p \implies q} \implies p} \implies p|1|2|3|4|8}}
{{EndTableau}}