avewright/proofwiki-math huggingface dataset:
Theorem: Conditional is Left Distributive over Conjunction/Formulation 1

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

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/Formulation 1

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

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/Formulation 1

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

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/Formulation 1

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

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/Formulation 2/Forward Implication

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

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/Formulation 2/Reverse Implication

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

Proof:
Let us use the following abbreviations
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text {for}
      | r = \paren {p \implies q} \land \paren {p \implies r}
      | c = 
}}
{{eqn | l = \psi
      | o = \text {for}
      | r = p \implies \paren {q \land 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 {\paren {p \implies q} \land \paren {p \implies r} } \implies \paren {p \implies \paren {q \land r} }$
{{qed}}
Theorem: Conditional is Left Distributive over Conjunction/Formulation 2

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

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/Formulation 2

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

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/Formulation 2

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

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}}
Theorem: Conditional is Left Distributive over Conjunction/Formulation 2

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

Proof:
Let us use the following abbreviations
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text {for}
      | r = \paren {p \implies q} \land \paren {p \implies r}
      | c = 
}}
{{eqn | l = \psi
      | o = \text {for}
      | r = p \implies \paren {q \land 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 {\paren {p \implies q} \land \paren {p \implies r} } \implies \paren {p \implies \paren {q \land r} }$
{{qed}}
Theorem: Criterion for Ring with Unity to be Topological Ring

Let $\struct {R, +, \circ}$ be a ring with unity.
Let $\tau$ be a topology over $R$.
Suppose that $+$ and $\circ$ are $\tau$-continuous mappings.
Then $\struct {R, +, \circ, \tau}$ is a topological ring.

Proof:
As we presume $\circ$ to be continuous, we need only prove that $\struct {R, +, \tau}$ is a topological group.
As we presume $+$ to be continuous, we need only show that negation is continuous.
As $\struct {R, \circ}$ is a semigroup and $\circ$ is continuous:
:$\struct{R, \circ, \tau}$ is a topological semigroup.
From Identity Mapping is Homeomorphism, the identity mapping $I_R : \struct {R, \tau} \to \struct {R, \tau}$ is continuous.
From Multiple Rule for Continuous Mappings to Topological Semigroup, the mapping $\paren{- 1_R} \circ I_R : R \to R$ defined by:
:$\forall b \in R : \map {\paren {\paren {-1_R} \circ I_R} } b = \paren {-1_R} \circ b$
is continuous.
From Product with Ring Negative, for each $b \in R : -b = \paren {-1_R} \circ b$.
Hence negation is continuous.
{{qed}}
i43n6rn55jasvjiw2e43wgnc6882ov7
Theorem: Union of Relations is Relation

Let $S$ and $T$ be sets.
Let $\FF$ be a family of relations from $S$ to $T$.
Let $\ds \RR = \bigcup \FF$, the union of all the elements of $\FF$.
Then $\RR$ is a relation from $S$ to $T$.
{{expand|Binary case}}

Proof:
By the definition of a relation from $S$ to $T$, each element of $\FF$ is a subset of $S \times T$.
By Union of Subsets is Subset: Set of Sets:
:$\RR \subseteq S \times T$
Therefore, by the definition of a relation from $S$ to $T$, $\RR$ is a relation from $S$ to $T$.
{{qed}}
Category:Relation Theory
703ie71rc52tci47k04ovl239sncgip
Theorem: Complex-Differentiable Function is Continuous

Let $f: D \to \C$ be a complex function, where $D \subseteq \C$ is an open set.
Let $f$ be complex-differentiable at $a \in D$.
Then $f$ is continuous at $a$.

Proof:
Let $\map {N_r} 0$ denote the $r$-neighborhood of $0$ in $\C$.
By the Epsilon-Function Complex Differentiability Condition, it follows that there exists $r \in \R_{>0}$ such that for all $h \in \map {N_r} 0 \setminus \set 0$:
:$(1): \quad \map f {a + h} = \map f a + h \paren {\map {f'} a + \map \epsilon h}$
where $\epsilon: \map {N_r} 0 \setminus \set 0 \to \C$ is a complex function with $\ds \lim_{h \mathop \to 0} \map \epsilon h = 0$.
We rewrite the {{RHS}} of $(1)$ to get:
{{begin-eqn}}
{{eqn | l = \map f {a + h}
      | r = \map f a + h \map {f'} a + h \map \epsilon h
}}
{{eqn | ll= \leadsto
      | l = \map f z 
      | r = \map f a + \paren {z - a} \map {f'} a + \paren {z - a} \map \epsilon {z - a}
      | c = substituting $z = a + h$ for $z \in \map {N_r} a$
}}
{{eqn | ll= \leadsto
      | l = \lim_{z \mathop \to a} \map f z
      | r = \lim_{z \mathop \to a} \paren {\map f a + \paren {z - a} \map {f'} a + \paren {z - a} \map \epsilon {z - a} }
      | c = Take the limit on both sides
}}
{{eqn | r = \map f a + \lim_{z \mathop \to a} \paren {z - a} \map {f'} a + \lim_{z \mathop \to a} \paren {\paren {z - a} \map \epsilon {z - a} }
      | c = Combination Theorem for Limits of Complex Functions
}}
{{eqn | r = \map f a
      | c = as $\ds \lim_{z \mathop \to a} \paren {z - a} = 0$, and $\ds \lim_{z \mathop \to a} \map \epsilon {z - a} = 0$
}}
{{end-eqn}}
By definition of continuous complex function, it follows that $f$ is continuous at $a$.
{{qed}}
Theorem: Complex-Differentiable Function is Continuous

Let $f: D \to \C$ be a complex function, where $D \subseteq \C$ is an open set.
Let $f$ be complex-differentiable at $a \in D$.
Then $f$ is continuous at $a$.

Proof:
For each $z \in D$:
{{begin-eqn}}
{{eqn | l = \lim_{w \mathop \to z} \map f w
      | r = \map f z + \lim_{w \mathop \to z} \paren {\map f w - \map f z}
      | c = Sum Rule for Limits of Complex Functions
}}
{{eqn | r = \map f z + \lim_{w \mathop \to z} \paren {\frac {\map f w - \map f z} {w - z} \paren {w - z} }
}}
{{eqn | r = \map f z + \lim_{w \mathop \to z} \frac {\map f w - \map f z} {w - z} \lim_{w \mathop \to z} \paren {w - z}
      | c = Product Rule for Limits of Complex Functions
}}
{{eqn | r = \map f z + \map {f'} z \cdot 0
      | c = {{Defof|Complex-Differentiable Function}}
}}
{{eqn | r = \map f z
}}
{{end-eqn}}
{{qed}}
Theorem: Proof by Cases/Formulation 1/Forward Implication/Proof 1

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

Proof:
{{BeginTableau|\paren {p \implies r} \land \paren {q \implies r} \vdash \paren {p \lor q} \implies r}}
{{Premise|1|\paren {p \implies r} \land \paren {q \implies r} }}
{{Simplification|2|1|p \implies r|1|1}}
{{Simplification|3|1|q \implies r|1|2}}
{{SequentIntro|4|1|p \lor q \implies r \lor r|2, 3|Constructive Dilemma}}
{{Assumption|5|p \lor q}}
{{ModusPonens|6|1, 5|r \lor r|4|5}}
{{Idempotence|7|1, 5|r|6|Disjunction}}
{{Implication|8|1|p \lor q \implies r|5|7}}
{{EndTableau}}
{{Qed}}
Theorem: Closed Ball in Euclidean Space is Compact

Let $x \in \R_n$ be a point in the Euclidean space $\R^n$.
Let $\epsilon \in \R_{>0}$.
Then the closed $\epsilon$-ball $\map {B_\epsilon^-} x$ is compact.

Proof:
From Closed Ball is Closed in Metric Space, it follows that $\map {B_\epsilon^-} x$ is closed in $\R^n$.
For all $a \in \map {B_\epsilon^-} x$ we have $\map d {x, a} \le \epsilon$, where $d$ denotes the Euclidean metric.
Then $\map {B_\epsilon^-} x$ is bounded in $\R^n$.
From the Heine-Borel Theorem, it follows that $\map {B_\epsilon^-} x$ is compact.
{{qed}}
Category:Closed Balls
Category:Compact Topological Spaces
Category:Euclidean Spaces
oxqckno428kmrygdm1dbxbonbd4tpfb
Theorem: Isometric Image of Cauchy Sequence is Cauchy Sequence

Let $\struct {S_1, d_1}$ and $\struct {S_2, d_2}$ be metric spaces.
Let $f: S_1 \to S_2$ be an isometry.
Let $\sequence {x_n}$ be a Cauchy sequence in $S_1$.
Let $\sequence {y_n} = \sequence {\map f {x_n} }$ be the image of $\sequence {x_n}$ under $f$.
Then $\sequence {y_n}$ is a Cauchy sequence.

Proof:
Let $\epsilon \in \R_{>0}$.
By the definition of Cauchy sequence, there is an $N \in \R$ such that:
:$\paren{m > N} \land \paren {n > N} \implies \map {d_1} {x_m, x_n} < \epsilon$
Since $f$ is an isometry, $\map {d_2} {y_m , y_n} = \map {d_1} {x_m, x_n}$ for all $m$ and $n$.
Thus:
:$\paren {m > N} \land \paren {n > N} \implies \map {d_2} {y_m, y_n} < \epsilon$
Hence $\sequence {y_n}$ is a Cauchy sequence.
{{qed}}
Category:Isometries (Metric Spaces)
Category:Cauchy Sequences
m2hhjtpbjmluaasw0o27xhtlful1zmm
Theorem: Union of Subsets is Subset

Let $S_1$, $S_2$, and $T$ be sets.
Let $S_1$ and $S_2$ both be subsets of $T$.
Then:
:$S_1 \cup S_2 \subseteq T$
That is:
:$\paren {S_1 \subseteq T} \land \paren {S_2 \subseteq T} \implies \paren {S_1 \cup S_2} \subseteq T$

Proof:
Let:
:$\paren {S_1 \subseteq T} \land \paren {S_2 \subseteq T}$
Then:
{{begin-eqn}}
{{eqn | l = S_1 \cup S_2
      | o = \subseteq
      | r = T \cup T
      | c = Set Union Preserves Subsets
}}
{{eqn | ll= \leadsto
      | l = S_1 \cup S_2
      | o = \subseteq
      | r = T
      | c = Set Union is Idempotent
}}
{{end-eqn}}
{{qed}}
Theorem: Union of Subsets is Subset

Let $S_1$, $S_2$, and $T$ be sets.
Let $S_1$ and $S_2$ both be subsets of $T$.
Then:
:$S_1 \cup S_2 \subseteq T$
That is:
:$\paren {S_1 \subseteq T} \land \paren {S_2 \subseteq T} \implies \paren {S_1 \cup S_2} \subseteq T$

Proof:
Let $x \in S_1 \cup S_2$.
By the definition of union, either $x \in S_1$ or $x \in S_2$.
By hypothesis, $S_1 \subseteq T$ and $S_2 \subseteq T$.
By definition of subset:
:$x \in S_1 \implies x \in T$
:$x \in S_2 \implies x \in T$
By Proof by Cases it follows that $x \in T$.
Hence the result by definition of subset.
{{qed}}
Theorem: Proof by Cases/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|\paren {p \implies r} \land \paren {q \implies r} \vdash \paren {p \lor q} \implies r}}
{{Premise|1|\paren {p \implies r} \land \paren {q \implies r} }}
{{Simplification|2|1|p \implies r|1|1}}
{{Simplification|3|1|q \implies r|1|2}}
{{SequentIntro|4|1|p \lor q \implies r \lor r|2, 3|Constructive Dilemma}}
{{Assumption|5|p \lor q}}
{{ModusPonens|6|1, 5|r \lor r|4|5}}
{{Idempotence|7|1, 5|r|6|Disjunction}}
{{Implication|8|1|p \lor q \implies r|5|7}}
{{EndTableau}}
{{Qed}}
Theorem: Proof by Cases/Formulation 1/Forward Implication

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

Proof:
From the Constructive Dilemma we have:
:$p \implies q, r \implies s \vdash p \lor r \implies q \lor s$
from which, changing the names of letters strategically:
:$p \implies r, q \implies r \vdash p \lor q \implies r \lor r$
From the Rule of Idempotence we have:
:$r \lor r \vdash r$
and the result follows by Hypothetical Syllogism.
{{qed}}
Theorem: Proof by Cases/Formulation 1

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

Proof:
{{BeginTableau|\paren {p \implies r} \land \paren {q \implies r} \vdash \paren {p \lor q} \implies r}}
{{Premise|1|\paren {p \implies r} \land \paren {q \implies r} }}
{{Simplification|2|1|p \implies r|1|1}}
{{Simplification|3|1|q \implies r|1|2}}
{{SequentIntro|4|1|p \lor q \implies r \lor r|2, 3|Constructive Dilemma}}
{{Assumption|5|p \lor q}}
{{ModusPonens|6|1, 5|r \lor r|4|5}}
{{Idempotence|7|1, 5|r|6|Disjunction}}
{{Implication|8|1|p \lor q \implies r|5|7}}
{{EndTableau}}
{{Qed}}
Theorem: Proof by Cases/Formulation 1

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

Proof:
From the Constructive Dilemma we have:
:$p \implies q, r \implies s \vdash p \lor r \implies q \lor s$
from which, changing the names of letters strategically:
:$p \implies r, q \implies r \vdash p \lor q \implies r \lor r$
From the Rule of Idempotence we have:
:$r \lor r \vdash r$
and the result follows by Hypothetical Syllogism.
{{qed}}
Theorem: Proof by Cases/Formulation 1

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

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.
:<nowiki>$\begin{array}{|ccccccc||ccccc|} \hline
(p & \implies & r) & \land & (q & \implies & r) & (p & \lor & q) & \implies & r \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \F & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \F & \F & \T & \F & \F & \F & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \T & \F & \F & \F \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Distance between Closed Sets in Euclidean Space

Let $S, T \subseteq \R^n$ be closed, non-empty subsets of the real Euclidean space $R^n$.
Suppose that $S$ is bounded, and $S$ and $T$ are disjoint.
Then there exists $x \in S$ and $y \in T$ such that:
:$\map d {x, y} = \map d {S, T} > 0$
where:
:$d$ denotes the Euclidean metric
:$\map d {S, T}$ is the distance between $S$ and $T$.

Proof:
By definition of distance from subset, we can for all $n \in \N$ find $x_n \in S, y_n \in T$ such that:
:$\map d {S, T} \le \map d {x_n, y_n} < \map d {S, T} + \dfrac 1 n$
so:
:$\ds \lim_{n \mathop \to \infty} \map d {x_n, y_n} = \map d {S, T}$
By definition of bounded space, there exists $a \in S$ and $K \in \R$ such that for all $x \in S$, we have $\map d {x, a} \le K$.
It follows that $\sequence {x_n}$ is a bounded sequence.
Then $\sequence {y_n}$ is also a bounded sequence, as:
{{begin-eqn}}
{{eqn | l = \map d {y_n, a}
      | o = \le
      | r = \map d {y_n, x_n} + \map d {x_n, a}
      | c = Triangle Inequality for Vectors in Euclidean Space
}}
{{eqn | o = <
      | r = \map d {S, T} + \dfrac 1 n + K
}}
{{eqn | o = \le
      | r = \map d {S, T} + 1 + K
}}
{{end-eqn}}
The sequence $\sequence {\tuple {x_n, y_n} }$ in $\R^{2 n}$ is also bounded, as:
{{begin-eqn}}
{{eqn | l = \map d {\tuple {x_n, y_n}, \tuple {a, a} }
      | r = \paren {\sum_{i \mathop = 1}^n \paren {x_i - a}^2 + \sum_{i \mathop = 1}^n \paren {y_i - a}^2}^{1 / 2}
      | c = {{Defof|Euclidean Metric on Real Vector Space}}
}}
{{eqn | o = \le
      | r = \sum_{i \mathop = 1}^n \paren {x_i - a}^2 + \sum_{i \mathop = 1}^n \paren {y_i - a}^2
      | c = by Minkowski's Inequality for Sums
}}
{{eqn | o = \le
      | r = 2 K + \map d {S, T} + 1 
}}
{{end-eqn}}
From Bounded Sequence in Euclidean Space has Convergent Subsequence, it follows that $\sequence {\tuple {x_n, y_n} }$ has a subsequence $\sequence {\tuple {x_{n_r}, y_{n_r} } }_{r \mathop \in N}$ that converges to a limit $\tuple {x, y} \in \R^{2n}$.
Then $\ds \lim_{r \mathop \to \infty} x_{n_r} = x$, and $\ds \lim_{r \mathop \to \infty} y_{n_r} = y$.
From Closed Set iff Contains all its Limit Points, it follows that $x \in S$, and $y \in T$.
Then from Distance Function of Metric Space is Continuous:
:$\ds \lim_{r \mathop \to \infty} \map d {x_{n_r}, y_{n_r} } = \map d {x, y}$
As a Convergent Sequence in Metric Space has Unique Limit, we have:
:$\ds \map d {x, y} = \lim_{r \mathop \to \infty} \map d {x_{n_r}, y_{n_r} } = \lim_{n \mathop \to \infty} \map d {x_n, y_n} = \map d {S, T}$
As $S$ and $T$ are disjoint, it follows that $x \ne y$.
Hence:
:$0 < \map d {x, y} = \map d {S, T}$
{{qed}}
Theorem: Complement in Distributive Lattice is Unique

Let $\struct {S, \vee, \wedge, \preceq}$ be a bounded distributive lattice.
Then every $a \in S$ admits at most one complement.

Proof:
Let $a \in S$, and suppose that $b, c \in S$ are complements for $a$.
Then:
{{begin-eqn}}
{{eqn | l = b
      | r = \top \wedge b
      | c = $\top$ is the identity for $\wedge$
}}
{{eqn | r = \paren {c \vee a} \wedge b
      | c = $c$ is a complement for $a$
}}
{{eqn | r = \paren {c \wedge b} \vee \paren {a \wedge b}
      | c = $S$ is a distributive lattice
}}
{{eqn | r = \paren {c \wedge b} \vee \bot
      | c = $b$ is a complement for $a$
}}
{{eqn | r = c \wedge b
      | c = $\bot$ is the identity for $\vee$
}}
{{end-eqn}}
Interchanging $c$ and $b$ in the above gives that $c = c \wedge b$ as well.
Hence $b = c$, as desired.
{{qed}}
Category:Distributive Lattices
Category:Bounded Lattices
bg1avy46njv0f82pk49jpdl2m5zuwfv
Theorem: Equivalence of Definitions of Top of Lattice

{{TFAE|def = Top of Lattice}}
Let $\struct {S, \vee, \wedge, \preceq}$ be a lattice.

Proof:
By definition, $\top$ is the greatest element of $S$ {{iff}} for all $a \in S$:
:$a \preceq \top$
By Ordering in terms of Meet, this is equivalent to:
:$a \wedge \top = a$
If this equality holds for all $a \in S$, then by definition $\top$ is an identity for $\wedge$.
The result follows.
{{qed}}
Category:Top of Lattice
lk3i35j6qhtebhpfa2huq86uo3upkmz
Theorem: Equivalence of Definitions of Bottom of Lattice

Let $\struct {S, \vee, \wedge, \preceq}$ be a lattice.
Let $\bot$ be a bottom of $\struct {S, \vee, \wedge, \preceq}$.
{{TFAE|def = Bottom of Lattice|view = Bottom|context = Lattice Theory}}

Proof:
By definition, $\bot$ is the smallest element of $S$ {{iff}} for all $a \in S$:
:$\bot \preceq a$
By Ordering in terms of Join, this is equivalent to:
:$a \vee \bot = a$
If this equality holds for all $a \in S$, then by definition $\bot$ is an identity for $\vee$.
The result follows.
{{qed}}
Category:Bottom of Lattice
6oynymwt4aogpco7ktmc574teg69eaf
Theorem: Top of Lattice is Unique

Let $\struct {S, \vee, \wedge, \preceq}$ be a lattice.
Then $S$ has at most one top.

Proof:
By definition, a top for $S$ is a greatest element.
The result follows from Greatest Element is Unique.
{{qed}}
Theorem: Bottom of Lattice is Unique

Let $\struct {S, \vee, \wedge, \preceq}$ be a lattice.
Then $S$ has at most one bottom.

Proof:
By definition, a bottom for $S$ is a smallest element.
The result follows from Smallest Element is Unique.
{{qed}}