avewright/proofwiki-math huggingface dataset:
Theorem: Transitive Relation Compatible with Semigroup Operation Relates Powers of Related Elements

Let $\struct {S, \circ}$ be a semigroup.
Let $\RR$ be a transitive relation on $S$ which is compatible with $\circ$.
Let $x, y \in S$ such that $x \mathrel \RR y$.
Let $n \in \N_{>0}$ be a strictly positive integer.
Then:
:$x^n \mathrel \RR y^n$
where $x^n$ is the $n$th power of $x$.

Proof:
We proceed by mathematical induction.
By definition of power:
:$x^1 = x$
:$y^1 = y$
Hence, by assumption:
:$x^1 \mathrel \RR y^1$
Suppose now that for $n \ge 1$:
:$x^n \mathrel \RR y^n$
Recall the assumption that $x \mathrel \RR y$.
Applying Operating on Transitive Relationships Compatible with Operation to these relations yields:
:$x^n \circ x \mathrel \RR y^n \circ y$
By definition of power:
:$x^{n + 1} = x^n \circ x$
and:
:$y^{n + 1} = y^n \circ y$
The result follows by the Principle of Mathematical Induction.
{{qed}}
Category:Compatible Relations
Category:Semigroups
k9jerwohrn7aehzulqtd6mth2c1idg8
Theorem: Reflexive Closure of Transitive Antisymmetric Relation is Ordering

Let $S$ be a set.
Let $\prec$ be a transitive, antisymmetric relation on $S$.
Let $\preceq$ be the reflexive closure of $\prec$.
Then $\preceq$ is an ordering on $S$.

Proof:
=== Reflexive ===
Follows from Reflexive Closure is Reflexive.
{{qed|lemma}}
Theorem: Reflexive Closure of Transitive Relation is Transitive

Let $S$ be a set.
Let $\RR$ be a transitive relation.
Let $\RR^=$ be the reflexive closure of $\RR$.
Then $\RR^=$ is also transitive.

Proof:
Let $a, b, c \in S$.
Suppose that $a \mathrel {\RR^=} b$ and $b \mathrel {\RR^=} c$.
If $a = b$, then since $b \mathrel {\RR^=} c$, also $a \mathrel {\RR^=} c$.
If $b = c$, then since $a \mathrel {\RR^=} b$, also $a \mathrel {\RR^=} c$.
The only case that remains is that $a \ne b$ and $b \ne c$.
Then by the definition of $\RR^=$, $a \mathrel \RR b$ and $b \mathrel \RR c$.
Since $\RR$ is transitive, it follows that:
:$a \mathrel \RR c$
and hence also $a \mathrel {\RR^=} c$.
Thus $\RR^=$ is transitive.
{{qed}}
Theorem: Reflexive Closure of Antisymmetric Relation is Antisymmetric

Let $S$ be a set.
Let $RR$ be an antisymmetric relation on $S$.
Let $\RR^=$ be the reflexive closure of $\RR$.
Then $\RR^=$ is also antisymmetric.

Proof:
Let $a, b \in S$.
Suppose that $a \mathrel {\RR^=} b$ and $b \mathrel {\RR^=} a$.
By definition of $\RR^=$, this means:
:$a \mathrel \RR b$ or $a = b$
:$b \mathrel \RR a$ or $b = a$
If $a = b$ or $b = a$ we are done, by definition of an antisymmetric relation.
So suppose $a \mathrel \RR b$ and $b \mathrel \RR a$.
Because $\RR$ is antisymmetric, it follows that $a = b$ in this case as well.
Hence $\RR^=$ is also antisymmetric.
{{qed}}
Category:Reflexive Closures
jd51zb94s9puvrye9syqfu52rt02gzd
Theorem: Positive Infinity is Greatest Element

Let $\left({\overline \R, \le}\right)$ be the extended real numbers with their usual ordering.
Then $+\infty$ is the greatest element of $\overline \R$.

Proof:
We have, by definition of the usual ordering on $\overline \R$:
:$\forall x \in \overline \R: x \le +\infty$
That is, $+\infty$ is the greatest element of $\overline \R$.
{{qed}}
Theorem: Negative Infinity is Smallest Element

Let $\left({\overline \R, \le}\right)$ be the extended real numbers with their usual ordering.
Then $-\infty$ is the smallest element of $\overline \R$.

Proof:
We have, by definition of the usual ordering on $\overline \R$:
:$\forall x \in \overline \R: -\infty \le x$
That is, $-\infty$ is the smallest element of $\overline \R$.
{{qed}}
Theorem: Relation Compatible with Group Operation is Strongly Compatible/Corollary

:$\forall x, y \in G:$
::$(1): \quad x \mathrel \RR y \iff e \mathrel \RR y \circ x^{-1}$
::$(2): \quad x \mathrel \RR y \iff e \mathrel \RR x^{-1} \circ y$
::$(3): \quad x \mathrel \RR y \iff x \circ y^{-1} \mathrel \RR e$
::$(4): \quad x \mathrel \RR y \iff y^{-1} \circ x \mathrel \RR e$

Proof:
Applying Relation Compatible with Group Operation is Strongly Compatible to $x$, $y$, and $x^{-1}$ we obtain:
:$x \mathrel \RR y \iff x \circ x^{-1} \mathrel \RR y \circ x^{-1}$
:$x \mathrel \RR y \iff x^{-1} \circ x \mathrel \RR x^{-1} \circ y$
Applying Relation Compatible with Group Operation is Strongly Compatible to $x$, $y$, and $y^{-1}$, on the other hand, yields:
:$x \mathrel \RR y \iff x \circ y^{-1} \mathrel \RR y \circ y^{-1}$
:$x \mathrel \RR y \iff y^{-1} \circ x \mathrel \RR y^{-1} \circ y$
By the definition of inverse element:
:$x \circ x^{-1} = x^{-1} \circ x = y \circ y^{-1} = y^{-1} \circ y = e$
Making these substitutions proves the theorem.
{{qed}}
Category:Relations Compatible with Group Operation
cj3f2techywn9y9l30y2bdjcgxrf8cl
Theorem: Dual Pairs (Order Theory)

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $a, b \in S$, and let $T \subseteq S$.
Then the following phrases about, and concepts pertaining to $\left({S, \preceq}\right)$ are dual to one another:
:{| style="text-align:center"
| $b \preceq a$
| width = "20px" |
| $a \preceq b$
|-
| $a$ succeeds $b$
|
| $a$ precedes $b$
|-
| $a$ strictly succeeds $b$
|
| $a$ strictly precedes $b$
|-
| $a$ is an upper bound for $T$
|
| $a$ is a lower bound for $T$
|-
| $a$ is a supremum for $T$
|
| $a$ is an infimum for $T$
|-
| $a$ is a maximal element of $T$
|
| $a$ is a minimal element of $T$
|-
| $a$ is the greatest element
|
| $a$ is the smallest element
|-
| the weak lower closure $a^\preceq$ of $a$
|
| the weak upper closure $a^\succeq$ of $a$
|-
| the strict lower closure $a^\prec$ of $a$
|
| the strict upper closure $a^\succ$ of $a$
|-
| the strict lower closure $T^\prec$ of $T$
|
| the strict upper closure $T^\succ$ of $T$
|-
| the join $a \vee b$ of $a$ and $b$
|
| the meet $a \wedge b$ of $a$ and $b$
|-
| $T$ is a lower section in $S$
|
| $T$ is an upper section in $S$
|-
| $\struct{S, \vee, \preceq}$ is a join semilattice
|
| $\struct{S, \wedge, \preceq}$ is a meet semilattice
|-
| $\struct{S, \preceq}$ is a complete join semilattice
|
| $\struct{S, \preceq}$ is a complete meet semilattice
|-
| $a$ is a join irreducible element
|
| $a$ is a meet irreducible element
|-
| $a$ is a join prime element
|
| $a$ is a meet prime element
|-
| $T$ is a filter of $\struct {S, \preceq}$
|
| $T$ is an ideal of $\struct {S, \preceq}$
|-
| $T$ is a completely prime ideal of $\struct{S, \preceq}$
|
| $T$ is a completely prime filter of $\struct{S, \preceq}$
|}

Proof:
Let $\succeq$ be the dual ordering of $\preceq$.
By definition of dual statement:
:$b \preceq a$
is dual to:
:$b \succeq a$
and by definition of dual ordering, this is equivalent to:
:$a \preceq b$
By virtue of Dual of Dual Statement (Order Theory), the converse follows.
The other claims are proved on the following pages, in order:
:Succeed is Dual to Precede
:Strictly Succeed is Dual to Strictly Precede
:Upper Bound is Dual to Lower Bound
:Supremum is Dual to Infimum
:Maximal Element is Dual to Minimal Element
:Greatest Element is Dual to Smallest Element
:Weak Lower Closure is Dual to Weak Upper Closure
:Strict Lower Closure is Dual to Strict Upper Closure
:Join is Dual to Meet
:Lower Section is Dual to Upper Section
:Join Semilattice is Dual to Meet Semilattice
:Complete Join Semilattice is Dual to Complete Meet Semilattice
:Join Irreducible Element is Dual of Meet Irreducible Element
:Join Prime Element is Dual of Meet Prime Element
:Ideal is Dual of Filter (Order Theory)
:Completely Prime Ideal is Dual of Completely Prime Filter
{{ProofWanted|For $T^\prec$}}
{{qed}}
Theorem: Conditional is not Right Self-Distributive/Formulation 1

While this holds:
:$\paren {p \implies q} \implies r \vdash \paren {p \implies r} \implies \paren {q \implies r}$
its converse does not:
:$\paren {p \implies r} \implies \paren {q \implies r} \not \vdash \paren {p \implies q} \implies r$

Proof:
We apply the Method of Truth Tables to the proposition:
:$\paren {p \implies q} \implies r \vdash \paren {p \implies r} \implies \paren {q \implies r}$
As can be seen for all boolean interpretations by inspection, where the truth value under the main connective on the {{LHS}} is $\T$, that under the one on the {{RHS}} is also $\T$:
$\begin{array}{|ccccc||ccccccc|} \hline
(p & \implies & q) & \implies & r & (p & \implies & r) & \implies & (q & \implies & r) \\
\hline
\F & \T & \F & \F & \F & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \F & \T & \F & \F & \T & \F & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \T \\
\T & \F & \F & \T & \F & \T & \F & \F & \T & \F & \F & \F \\
\T & \F & \F & \T & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \T & \T & \F & \F & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed|lemma}}
The two formulas are not equivalent, as the relevant columns do not match exactly.
For example, when $p =  q = r = \F$ we have that:
:$\paren {p \implies q} \implies r = \F$
but:
:$\paren {p \implies r} \implies \paren {q \implies r} = \T$
Hence the result:
:$\paren {p \implies q} \implies r \vdash \paren {p \implies r} \implies \paren {q \implies r}$
but:
:$\paren {p \implies r} \implies \paren {q \implies r} \not \vdash \paren {p \implies q} \implies r$
{{qed}}
Category:Truth Table Proofs
Category:Conditional is not Right Self-Distributive
i2i9uqfsona78nmvdj48zs5uaq5achx
Theorem: Conditional is not Right Self-Distributive/Formulation 2

While this holds:
:$\vdash \paren {\paren {p \implies q} \implies r} \implies \paren {\paren {p \implies r} \implies \paren {q \implies r} }$
its converse does not:
:$\not \vdash \paren {\paren {p \implies r} \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies r}$

Proof:
{{ProofWanted|Can be seen to be logically equivalent to Conditional is not Right Self-Distributive/Formulation 1 by application of the Rule of Implication and Modus Ponendo Ponens.}}
Theorem: Cauchy-Riemann Equations

Let $D \subseteq \C$ be an open subset of the set of complex numbers $\C$.
Let $f: D \to \C$ be a complex function on $D$.
Let $u, v: \set {\tuple {x, y} \in \R^2: x + i y = z \in D} \to \R$ be the two real-valued functions defined as:
{{begin-eqn}}
{{eqn | l = \map u {x, y}
      | r = \map \Re {\map f z}
}}
{{eqn | l = \map v {x, y}
      | r = \map \Im {\map f z}
}}
{{end-eqn}}
where:
:$\map \Re {\map f z}$ denotes the real part of $\map f z$
:$\map \Im {\map f z}$ denotes the imaginary part of $\map f z$.
Then $f$ is complex-differentiable in $D$ {{iff}}:
:$u$ and $v$ are differentiable in their entire domain
and:
:The following two equations, known as the '''Cauchy-Riemann equations''', hold for the continuous partial derivatives of $u$ and $v$:
{{begin-eqn}}
{{eqn | n = 1
      | l = \dfrac {\partial u} {\partial x}
      | r = \dfrac {\partial v} {\partial y}
}}
{{eqn | n = 2
      | l = \dfrac {\partial u} {\partial y}
      | r = -\dfrac {\partial v} {\partial x}
}}
{{end-eqn}}
{{ExtractTheorem|This relates to the final $3$rd part of this page: Cauchy-Riemann Equations/Expression of Derivative. Needs to be separated out properly.}}
If the conditions are true, then for all $z \in D$:
:$\map {f'} z = \map {\dfrac {\partial f} {\partial x} } z = -i \map {\dfrac {\partial f} {\partial y} } z$

Proof:
=== Necessary Condition ===
{{:Cauchy-Riemann Equations/Necessary Condition}}{{qed|lemma}}
Theorem: Self-Distributive Law for Conditional/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \iff \paren {\paren {p \implies q} \implies \paren {p \implies r} } }}
{{TheoremIntro|1|\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }|Self-Distributive Law for Conditional: Formulation 2: Forward Implication}}
{{TheoremIntro|2|\paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|Self-Distributive Law for Conditional: Formulation 2: Reverse Implication}}
{{BiconditionalIntro|3||\paren {p \implies \paren {q \implies r} } \iff \paren {\paren {p \implies q} \implies \paren {p \implies r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 2

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

Proof:
{{BeginTableau|\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} } }}
{{Assumption  |1|p \implies \paren {q \implies r} }}
{{SequentIntro|2|1|\paren {p \implies q} \implies \paren {p \implies r}|1|Self-Distributive Law for Conditional: Formulation 1}}
{{Implication |3||\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 2

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

Proof:
{{BeginTableau|\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} } }}
{{Assumption  |1|p \implies \paren {q \implies r} }}
{{Assumption  |2|p \implies q}}
{{Assumption  |3|p}}
{{ModusPonens |4|1,3|q \implies r|1|3}}
{{ModusPonens |5|2,3|q|2|3}}
{{ModusPonens |6|1,2,3|r|4|5}}
{{Implication |7|1,2|p \implies r|3|6}}
{{Implication |8|1|\paren {p \implies q} \implies \paren {p \implies r}|2|7}}
{{Implication |9||\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }|1|8}}
{{EndTableau}}
{{Qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 2

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth value under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|ccccccc|}
\hline
(p & \implies & (q & \implies & r)) & \implies & ((p & \implies & q) & \implies & (p & \implies & r)) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \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 & \T & \F & \T & \F & \T & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \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>
Theorem: Self-Distributive Law for Conditional/Formulation 2

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

Proof:
{{BeginTableau |\vdash \paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption   |1|\paren {p \implies q} \implies \paren {p \implies r} }}
{{SequentIntro |2|1|p \implies \paren {q \implies r}|1|Self-Distributive Law for Conditional: Formulation 1}}
{{Implication  |3||\paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 2

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

Proof:
{{BeginTableau |\vdash \paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption|1|\paren {p \implies q} \implies \paren {p \implies r} }}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{SequentIntro|4|3|p \implies q|3|True Statement is implied by Every Statement}}
{{ModusPonens|5|1, 3|p \implies r|1|4}}
{{ModusPonens|6|1, 2, 3|r|5|2}}
{{Implication|7|1, 2|q \implies r|3|6}}
{{Implication|8|1|p \implies \paren {q \implies r}|2|7}}
{{Implication|9||\paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|1|8}}
{{EndTableau|qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 1

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

Proof:
{{BeginTableau|p \implies \paren {q \implies r} \vdash \paren {p \implies q} \implies \paren {p \implies r} }}
{{Premise|1|p \implies \paren {q \implies r} }}
{{Assumption|2|p \implies q}}
{{Assumption|3|p}}
{{ModusPonens|4|1, 3|q \implies r|1|3}}
{{ModusPonens|5|2, 3|q|2|3}}
{{ModusPonens|6|1, 2, 3|r|4|5}}
{{Implication|7|1, 2|p \implies r|3|6}}
{{Implication|8|1|\paren {p \implies q} \implies \paren {p \implies r}|2|7}}
{{EndTableau|qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 1

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

Proof:
We apply the Method of Truth Tables to the proposition:
$p \implies \paren {q \implies r} \dashv \vdash \paren {p \implies q} \implies \paren {p \implies r}$
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 & \implies & r) & (p & \implies & q) & \implies & (p & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \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 & \T & \F & \T & \F & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \F & \F & \T & \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: Self-Distributive Law for Conditional/Formulation 1

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

Proof:
{{BeginTableau|\paren {p \implies q} \implies \paren {p \implies r} \vdash p \implies \paren {q \implies r} }}
{{Premise|1|\paren {p \implies q} \implies \paren {p \implies r} }}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{SequentIntro|4|3|p \implies q|3|True Statement is implied by Every Statement}}
{{ModusPonens|5|1, 3|p \implies r|1|4}}
{{ModusPonens|6|1, 2, 3|r|5|2}}
{{Implication|7|1, 2|q \implies r|3|6}}
{{Implication|8|1|p \implies \paren {q \implies r}|2|7}}
{{EndTableau}}
{{qed}}
Theorem: Cauchy-Riemann Equations/Expression of Derivative

Let $D \subseteq \C$ be an open subset of the set of complex numbers $\C$.
Let $f: D \to \C$ be a complex function on $D$.
Let $u, v: \set {\tuple {x, y} \in \R^2: x + i y = z \in D} \to \R$ be two real-valued functions defined as:
{{begin-eqn}}
{{eqn | l = \map u {x, y}
      | r = \map \Re {\map f z}
}}
{{eqn | l = \map v {x, y}
      | r = \map \Im {\map f z}
}}
{{end-eqn}}
where:
:$\map \Re {\map f z}$ denotes the real part of $\map f z$
:$\map \Im {\map f z}$ denotes the imaginary part of $\map f z$.
Then $f$ is complex-differentiable in $D$ {{iff}}:
:$u$ and $v$ are differentiable in their entire domain
and:
:The following two equations, known as the '''Cauchy-Riemann equations''', hold for the partial derivatives of $u$ and $v$:
{{begin-eqn}}
{{eqn | n = 1
      | l = \dfrac {\partial u} {\partial x}
      | r = \dfrac {\partial v} {\partial y}
}}
{{eqn | n = 2
      | l = \dfrac {\partial u} {\partial y}
      | r = -\dfrac {\partial v} {\partial x}
}}
{{end-eqn}}
If the conditions are true, then for all $z \in D$:
:$\map {f'} z = \map {\dfrac {\partial f} {\partial x} } z = -i \map {\dfrac {\partial f} {\partial y} } z$
{{refactor|Extract "Cauchy-Riemann Equations" into a definition page}}

Proof:
Let $z = x + i y$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\dfrac {\partial f} {\partial x} } z
      | r = \map {\dfrac {\partial u} {\partial x} } {x, y} + i \map {\dfrac {\partial v} {\partial x} } {x, y}
}}
{{eqn | r = \map \Re {\map {f'} z} + i \, \map \Im {\map {f'} z}
      | c = from the last part of the proof for sufficient condition
}}
{{eqn | r = \map {f'} z
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = -i \map {\dfrac {\partial f} {\partial y} } z
      | r = -i \paren {\map {\dfrac {\partial u} {\partial y} } {x, y} + i \map {\dfrac {\partial v} {\partial y} } {x, y} }
}}
{{eqn | r = -i \paren {-\map \Im {\map {f'} z} + i \map \Re {\map {f'} z} }
      | c = from the last part of the proof for sufficient condition
}}
{{eqn | r = \map {f'} z
}}
{{end-eqn}}
{{qed}}
Theorem: Succeed is Dual to Precede

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $a, b \in S$.
The following are dual statements:
:$a$ succeeds $b$
:$a$ precedes $b$

Proof:
By definition, $a$ succeeds $b$ {{iff}}:
:$b \preceq a$
The dual of this statement is:
:$a \preceq b$
by Dual Pairs (Order Theory).
By definition, this means $a$ precedes $b$.
The converse follows from Dual of Dual Statement (Order Theory).
{{qed}}
Theorem: Strictly Succeed is Dual to Strictly Precede

Let $\struct {S, \preceq}$ be an ordered set.
Let $a, b \in S$.
The following are dual statements:
:$a$ strictly succeeds $b$
:$a$ strictly precedes $b$

Proof:
By definition, $a$ strictly succeeds $b$ {{iff}}:
:$b \preceq a$ and $b \ne a$
The dual of this statement is:
:$a \succeq b$ and $b \ne a$
by Dual Pairs (Order Theory).
By definition, this means $a$ strictly precedes $b$.
The converse follows from Dual of Dual Statement (Order Theory).
{{qed}}
Theorem: Upper Bound is Dual to Lower Bound

Let $\struct {S, \preceq}$ be an ordered set.
Let $a \in S$ and $T \subseteq S$.
The following are dual statements:
:$a$ is an upper bound for $T$
:$a$ is a lower bound for $T$

Proof:
By definition, $a$ is an upper bound for $T$ {{iff}}:
:$\forall t \in T: t \preceq a$
The dual of this statement is:
:$\forall t \in T: a \preceq t$
by Dual Pairs (Order Theory).
By definition, this means $a$ is a lower bound for $T$.
The converse follows from Dual of Dual Statement (Order Theory).
{{qed}}
Theorem: Supremum is Dual to Infimum

Let $\struct {S, \preceq}$ be an ordered set.
Let $a \in S$ and $T \subseteq S$.
The following are dual statements:
:$a$ is a supremum for $T$
:$a$ is an infimum for $T$

Proof:
By definition, $a$ is a supremum for $T$ {{iff}}:
:$a$ is an upper bound for $T$
:$a \preceq b$ for all upper bounds $b$ of $T$
The dual of this statement is:
:$a$ is a lower bound for $T$
:$b \preceq a$ for all lower bounds $b$ of $T$
by Dual Pairs (Order Theory).
By definition, this means $a$ is an infimum for $T$.
The converse follows from Dual of Dual Statement (Order Theory).
{{qed}}
Theorem: Maximal Element is Dual to Minimal Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$, and $a \in T$.
The following are dual statements:
:$a$ is a maximal element of $T$
:$a$ is a minimal element of $T$

Proof:
By definition, $a$ is a maximal element of $T$ {{iff}}:
:$\forall t \in T: a \preceq t$ implies $a = t$
The dual of this statement is:
:$\forall t \in T: t \preceq a$ implies $a = t$
by Dual Pairs (Order Theory).
By definition, this means $a$ is a minimal element of $T$.
The converse follows from Dual of Dual Statement (Order Theory).
{{qed}}
Theorem: Greatest Element is Dual to Smallest Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $a \in S$.
The following are dual statements:
:$a$ is the greatest element of $S$
:$a$ is the smallest element of $S$

Proof:
By definition, $a$ is the greatest element of $S$ {{iff}}:
:$\forall b \in S: b \preceq a$
The dual of this statement is:
:$\forall b \in S: a \preceq b$
by Dual Pairs (Order Theory).
By definition, this means $a$ is the smallest element of $S$.
The converse follows from Dual of Dual Statement (Order Theory).
{{qed}}