avewright/proofwiki-math huggingface dataset:
Theorem: Contour Integral is Well-Defined

Let $C$ be a contour defined by a finite sequence $C_1, \ldots, C_n$ of directed smooth curves in the complex plane $\C$.
Let $C_k$ be parameterized by the smooth path $\gamma_k: \closedint {a_k} {b_k} \to \C$ for all $k \in \set {1, \ldots, n}$.
Let $f: \Img C \to \C$ be a continuous complex function, where $\Img C$ denotes the image of $C$.
Let $\sigma_k: \closedint {c_k} {d_k} \to \C$ be a reparameterization of $C_k$ for all $k \in \set {1, \ldots, n}$.
Then:
:$\ds \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \map f {\map {\gamma_k} t} \map {\gamma_k'} t \rd t = \sum_{k \mathop = 1}^n \int_{c_k}^{d_k} \map f {\map {\sigma_k} t} \map {\sigma_k'} t \rd t$
and all complex Riemann integrals in the equation are defined.

Proof:
Define $g_k: \closedint {a_k} {b_k} \to \C$ by $\map {g_k} t = \map f {\map {\gamma_k} t} \map {\gamma_k'} t$ for all $k \in \set {1, \ldots, n}$.
By definition of smooth path, it follows that $\gamma_k$ and $\gamma_k'$ are continuous for all $k \in \set {1, \ldots, n}$.
From Continuity of Composite Mapping/Corollary and Sum Rule for Continuous Complex Functions, it follows that $g_k$ is continuous.
From Continuous Complex Function is Complex Riemann Integrable, we find that $\ds \int_{a_k}^{b_k} \map {g_k} t \rd t$ is defined.
Similarly, it can be shown that $\ds \int_{c_k}^{d_k} \map f {\map {\sigma_k} t} \map {\sigma_k'} t \rd t$ is defined for all $k \in \set {1, \ldots, n}$.
Hence, all complex Riemann integrals in the theorem are defined.
The equality now follows from Contour Integral is Independent of Parameterization.
{{qed}}
Theorem: Boolean Prime Ideal Theorem

Let $\struct {S, \le}$ be a Boolean lattice.
Let $I$ be an ideal in $S$.
Let $F$ be a filter on $S$.
Let $I \cap F = \O$.
Then there exists a prime ideal $P$ in $S$ such that:
:$I \subseteq P$
and:
:$P \cap F = \O$

Proof:
We prove that the Boolean Prime Ideal Theorem is equivalent to Stone's Representation Theorem for Boolean Algebras in ZF.
{{ProofWanted}}
Theorem: Central Limit Theorem

Let $X_1, X_2, \ldots$ be a sequence of independent and identically distributed real-valued random variables with:
:expectation $\expect {X_i} = \mu \in \R$
:variance $\var {X_i} = \sigma^2 > 0$
Let:
:$\ds S_n = \sum_{i \mathop = 1}^n X_i$
Then:
:$\dfrac {S_n - n \mu} {\sqrt {n \sigma^2} } \xrightarrow D \Gaussian 0 1$ as $n \to \infty$
that is, converges in distribution to a standard normal distribution.

Proof:
Let $Y_i = \dfrac {X_i - \mu} \sigma$.
We have that:
:$\expect {Y_i} = 0$
and:
:$\expect {Y_i^2} = 1$
Then by Taylor's Theorem the characteristic function can be written:
:$\map {\phi_{Y_i} } t = 1 - \dfrac {t^2} 2 + \map o {t^2}$
Now let:
{{begin-eqn}}
{{eqn | l = U_n 
      | r = \frac {S_n - n \mu} {\sqrt {n \sigma^2} }
}}
{{eqn | r = \sum_{i \mathop = 1}^n \frac {X_i - \mu} {\sqrt {n \sigma^2} } 
}}
{{eqn | r = \frac 1 {\sqrt n} \sum_{i \mathop = 1}^n \paren {\frac {X_i - \mu} \sigma} 
}}
{{eqn | r = \frac 1 {\sqrt n} \sum_{i \mathop = 1}^n Y_i 
}}
{{end-eqn}}
Then its characteristic function is given by:
{{begin-eqn}}
{{eqn | l = \map {\phi_{U_n} } t
      | r = \expect {e^{i t U_n} }
}}
{{eqn | r = \expect {\map \exp {\frac {i t} {\sqrt n} \sum_{i \mathop = 1}^n Y_i} }
}}
{{eqn | r = \prod_{i \mathop = 1}^n \expect {\map \exp {\frac{i t} {\sqrt n} Y_i} }
      | c = since $Y_i$ are independent and identically distributed
}}
{{eqn | r = \prod_{i \mathop = 1}^n \map {\phi_{Y_i} } {\frac t {\sqrt n} }
}}
{{eqn | r = \paren {\map {\phi_{Y_i} } {\frac t {\sqrt n} } }^n
      | c = since $Y_i$ are independent and identically distributed
}}
{{eqn | r = \paren {1 - \frac {t^2} {2 n} + \map o {t^2} }^n
}}
{{end-eqn}}
Recall that the Characteristic Function of Normal Distribution is given by:
{{begin-eqn}}
{{eqn | l = \map \phi t
      | r = e^{i t \mu - \frac 1 2 t^2 \sigma^2}
}}
{{eqn | r = e^{i t \paren 0 - \frac 1 2 t^2 \paren 1^2}
}}
{{eqn | r = e^{-\frac 1 2 t^2}
}}
{{end-eqn}}
Indeed, the characteristic function of $S_n$ converges to the Characteristic Function of Normal Distribution:
:$\paren {1 - \dfrac {t^2} {2 n} + \map o {t^2} }^n \to e^{-\frac 1 2 t^2}$ as $n \to \infty$
Then Lévy's Continuity Theorem applies.
In particular, the convergence in distribution of the $U_n$ to some random variable with standard normal distribution is equivalent to continuity of the limiting characteristic equation at $t = 0$.
But $e^{-\frac 1 2 t^2}$ is clearly continuous at $0$.
So we have that $\dfrac {S_n - n \mu} {\sqrt {n \sigma^2} }$ converges in distribution to a standard normal random variable.
{{qed}}
Theorem: Arcsine Logarithmic Formulation

For any real number $x: -1 \le x \le 1$:
:$\arcsin x = \dfrac 1 i \map \ln {i x + \sqrt {1 - x^2} }$
where $\arcsin x$ is the arcsine and $i^2 = -1$.

Proof:
Assume $y \in \R$ where $-\dfrac \pi 2 \le y \le \dfrac \pi 2$.
{{begin-eqn}}
{{eqn | l = y
      | r = \arcsin x
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \sin y
      | c = {{Defof|Real Arcsine}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \frac 1 {2 i} \paren {e^{i y} - e^{-i y} }
      | c = Euler's Sine Identity
}}
{{eqn | ll= \leadstoandfrom
      | l = 2 i x
      | r = e^{i y} - e^{-i y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 2 i x e^{i y}
      | r = e^{2 i y} - 1
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{2 i y} -2 i x e^{i y}
      | r = 1
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{2 i y} - 2 i x e^{i y} - x^2
      | r = 1 - x^2
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {e^{i y} - i x}^2
      | r = 1 - x^2
      | c = Square of Difference
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{i y} - i x
      | r = \sqrt {1 - x^2}
      | c = {{Defof|Square Root}}
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{i y}
      | r = i x + \sqrt {1 - x^2}
}}
{{eqn | ll= \leadstoandfrom
      | l = i y
      | r = \map \ln {i x + \sqrt {1 - x^2} }
      | c = {{Defof|Complex Natural Logarithm}}
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | r = \dfrac 1 i \map \ln {i x + \sqrt {1 - x^2} }
}}
{{end-eqn}}
{{qed}}
Theorem: Arccosine Logarithmic Formulation

For any real number $x: -1 \le x \le 1$:
:$\arccos x = \dfrac 1 i \map \ln {x + \sqrt {x^2 - 1} }$
where $\arccos x$ is the arccosine and $i^2 = -1$.

Proof:
Assume $y \in \R$ such that $0 \le y \le \pi$.
{{begin-eqn}}
{{eqn | l = y
      | r = \arccos x
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \cos y
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \frac 1 2 \paren {e^{-i y} + e^{i y} }
      | c = Euler's Cosine Identity
}}
{{eqn | ll= \leadstoandfrom
      | l = 2 x
      | r = e^{-i y} + e^{i y}
}}
{{eqn | ll= \leadstoandfrom
      | l = 2 x e^{i y}
      | r = 1 + e^{2 i y}
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{2 i y} - 2 x e^{i y}
      | r = -1
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{2 i y} - 2 x e^{i y} + x^2
      | r = x^2 - 1
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {e^{i y} - x}^2
      | r = x^2 - 1
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{i y} - x
      | r = \sqrt {x^2 - 1}
}}
{{eqn | ll= \leadstoandfrom
      | l = i y
      | r = \map \ln {x + \sqrt {x^2 - 1} }
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | r = \dfrac 1 i \map \ln {x + \sqrt {x^2 - 1} }
}}
{{end-eqn}}
{{qed}}
Theorem: Arctangent Logarithmic Formulation

For any real number $x$:
:$\arctan x = -\dfrac i 2 \map \ln {\dfrac {1 + i x} {1 - i x} }$
where $\arctan x$ is the arctangent and $i^2 = -1$.

Proof:
Assume $y \in \R$, $ -\dfrac \pi 2 \le y \le \dfrac \pi 2 $.
{{begin-eqn}}
{{eqn | l = y
      | r = \arctan x
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \tan y
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = i \frac {1 - e^{2 i y} } {1 + e^{2 i y} }
      | c = Euler's Tangent Identity
}}
{{eqn | ll= \leadstoandfrom
      | l = i x
      | r = \frac {e^{2 i y} - 1} {e^{2 i y} + 1}
      | c = $ i^2 = -1 $
}}
{{eqn | ll= \leadstoandfrom
      | l = i x \paren {e^{2 i y} + 1}
      | r = e^{2 i y} - 1
}}
{{eqn | ll= \leadstoandfrom
      | l = i x e^{2 i y} + i x
      | r = e^{2 i y} - 1
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{2 i y} - i x e^{2 i y}
      | r = 1 + i x
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{2 i y}
      | r = \frac {1 + i x} {1 - i x}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 2 i y
      | r = \map \ln {\frac {1 + i x} {1 - i x} }
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | r = \frac 1 {2 i} \map \ln {\frac {1 + i x} {1 - i x} }
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | r = \dfrac i i \times \dfrac 1 {2 i} \map \ln {\dfrac {1 + i x } {1 - i x } }
      | c = multiplying top and bottom by $i$
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | r = -\frac i 2 \map \ln {\frac {1 + i x} {1 - i x} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Length of Contour is Well-Defined

Let $C_1, \ldots, C_n$ be directed smooth curves.
Let $C_k$ be parameterized by the smooth path $\gamma_k: \closedint {a_k} {b_k} \to \C$ for all $k \in \set {1, \ldots, n}$.
Let $C$ be the contour defined by the finite sequence $C_1, \ldots, C_n$.
Suppose that $\sigma_k: \closedint {c_k} {d_k} \to \C$ is a reparameterization of $C_k$ for all $k \in \set {1, \ldots, n}$
Then:
:$\ds \sum_{k \mathop = 1}^n \int_{a_k }^{b_k} \size {\map {\gamma_k'} t} \rd t = \sum_{k \mathop = 1}^n \int_{c_k}^{d_k} \size {\map {\sigma_k'} t} \rd t$
and all real integrals in the equation are defined.

Proof:
From the definition of directed smooth curve, it follows that  $\sigma_k = \gamma_k \circ \phi_k$ for all $k \in \set {1, \ldots, n}$.
Here, $\phi_k: \closedint {c_k} {d_k} \to \closedint {a_k} {b_k}$ is a bijective differentiable strictly increasing function. 
For all $k \in \set {1, \ldots, n}$, $\gamma_k$ and $\sigma_k$ are continuous.
From Complex Modulus Function is Continuous and Continuity of Composite Mapping: Corollary, it follows that $\cmod {\gamma_k'}$ and $\cmod {\sigma_k'}$ are continuous.
From Continuous Real Function is Darboux Integrable, we find that $\ds \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \cmod {\map {\gamma_k'} t} \rd t$ and $\ds \sum_{k \mathop = 1}^n \int_{c_k}^{d_k} \cmod {\map {\sigma_k'} t} \rd t$ are defined.
Hence, all real integrals in the theorem are defined.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \int_{a_k }^{b_k} \cmod {\map {\gamma_k'} t} \rd t
      | r = \sum_{k \mathop = 1}^n \int_{\map {\phi_k^{-1} } {a_k} }^{\map {\phi_k^{-1} } {b_k} } \cmod {\map {\gamma_k'} {\map \phi u} } \map {\phi'} u \rd u
      | c = substitution with $t = \map \phi u$
}}
{{eqn | r = \sum_{k \mathop = 1}^n \int_{\map {\phi_k^{-1} } {a_k} }^{\map {\phi_k^{-1} } {b_k} } \cmod {\map {\gamma_k'} {\map \phi u} \map {\phi'} u}\rd u
      | c = as $\map {\phi'} u > 0$ by Derivative of Monotone Function
}}
{{eqn | r = \sum_{k \mathop = 1}^n \int_{\map {\phi_k^{-1} } {a_k} }^{\map {\phi_k^{-1} } {b_k} } \cmod {\map {\sigma'} u} \rd u
      | c = Derivative of Complex Composite Function
}}
{{eqn | r = \sum_{k \mathop = 1}^n \int_{c_k}^{d_k} \cmod {\map {\sigma'} u} \rd u
      | c = Reparameterization of Directed Smooth Curve Maps Endpoints To Endpoints
}}
{{end-eqn}}
{{qed}}
Category:Complex Contour Integrals
Category:Contour Integrals
lu9xa1ggsruum391l8hz15jvp7y2b9g
Theorem: Two Ring is Boolean Ring

Let $2$ be the two ring.
Then $2$ is a Boolean ring.

Proof:
From Ring of Integers Modulo m is Ring, $2$ is a ring with unity.
Furthermore, the identities:
:$0 \cdot 0 = 0$
:$1 \cdot 1 = 1$
show that $2$ is also an idempotent ring.
Hence the result, by definition of Boolean ring.
{{qed}}
Theorem: Idempotent Ring is Commutative

Let $\struct {R, +, \circ}$ be an idempotent ring.
Denote with $0_R$ the zero of $R$.
Then $\struct {R, +, \circ}$ is a commutative ring.

Proof:
Let $x, y \in R$.
Then:
{{begin-eqn}}
{{eqn | l = x + y
      | r = \paren {x + y}^2
      | c = {{Defof|Idempotent Ring}}
}}
{{eqn | r = x^2 + x \circ y + y \circ x + y^2
      | c = Binomial Theorem: Ring Theory
}}
{{eqn | r = x + x \circ y + y \circ x + y
      | c = {{Defof|Idempotent Ring}}
}}
{{end-eqn}}
Subtracting $x + y$ from both sides yields:
{{begin-eqn}}
{{eqn | l = x \circ y + y \circ x
      | r = 0_R
}}
{{eqn | r = y \circ x + y \circ x
      | c = Idempotent Ring has Characteristic Two
}}
{{end-eqn}}
Finally, subtracting $y \circ x$ from both sides, we obtain:
:$x \circ y = y \circ x$
and conclude $R$ is a commutative ring.
{{qed}}
Theorem: Idempotent Ring has Characteristic Two

Let $\struct {R, +, \circ}$ be an idempotent non-null ring.
Denote with $0_R$ the zero of $R$.
Then $\struct {R, +, \circ}$ has characteristic $2$.

Proof:
Let $x \in R$.
Then:
{{begin-eqn}}
{{eqn | l = x + x
      | r = \paren {x + x}^2
      | c = {{Defof|Idempotent Ring}}
}}
{{eqn | r = \paren {x + x} \paren {x + x}
}}
{{eqn | r = x \paren {x + x} + x \paren {x + x}
      | c = {{Ring-axiom|D}}
}}
{{eqn | r = x^2 + x^2 + x^2 + x^2
      | c = {{Ring-axiom|D}} again
}}
{{eqn | r = x + x + x + x
      | c = {{Defof|Idempotent Ring}}
}}
{{eqn | ll= \leadsto
      | l = 0_R
      | r = x + x
      | c = $\struct {\R, +}$ is a group, so Cancellation Laws apply
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Two-Valued Functions form Boolean Ring

Let $S$ be a set, and let $2$ be the two ring.
Let $2^S$ be the set of all $2$-valued functions on $S$.
Denote with $+$ and $\cdot$ the pointwise operations induced on $2^S$ by $+_2$ and $\times_2$, respectively.
Then $\struct {2^S, +, \cdot}$ is a Boolean ring.

Proof:
By Structure Induced by Ring Operations is Ring, $\struct {2^S, +, \cdot}$ is a ring.
By Unity of Induced Structure, $\struct {2^S, +, \cdot}$ also has a unity.
By Induced Structure is Idempotent, $\cdot$ is an idempotent operation.
Hence $\struct {2^S, +, \cdot}$ is a Boolean ring.
{{qed}}
Theorem: Complex Integration by Substitution

Let $\closedint a b$ be a closed real interval.
Let $\phi: \closedint a b \to \R$ be a real function which has a derivative on $\closedint a b$.
Let $f: A \to \C$ be a continuous complex function, where $A$ is a subset of the image of $\phi$.
If $\map \phi a \le \map \phi b$, then:
:$\ds \int_{\map \phi a}^{\map \phi b} \map f t \rd t = \int_a^b \map f {\map \phi u} \map {\phi'} u \rd u$
If $\map \phi a > \map \phi b$, then:
:$\ds \int_{\map \phi b}^{\map \phi a} \map f t \rd t = -\int_a^b \map f {\map \phi u} \map {\phi'} u \rd u$

Proof:
Let $\Re$ and $\Im$ denote real parts and imaginary parts respectively.
Let $\map \phi a \le \map \phi b$.
Then:
{{begin-eqn}}
{{eqn | l = \int_{\map \phi a}^{\map \phi b} \map f t \rd t
      | r = \int_{\map \phi a}^{\map \phi b} \map \Re {\map f t} \rd t + i \int_{\map \phi a}^{\map \phi b} \map \Im {\map f t} \rd t
      | c = {{Defof|Complex Riemann Integral}}
}}
{{eqn | r = \int_a^b \map \Re {\map f {\map \phi u} } \map {\phi'} u \rd u + i \int_a^b \map \Im {\map f {\map \phi u} } \map {\phi'} u \rd u
      | c = Integration by Substitution: Definite Integral
}}
{{eqn | r = \int_a^b \map \Re {\map f {\map \phi u} \map {\phi'} u} \rd u + i \int_a^b \map \Im {\map f {\map \phi u} \map {\phi'} u} \rd u
      | c = Multiplication of Real and Imaginary Parts
}}
{{eqn | r = \int_a^b \map f {\map \phi u} \map {\phi'} u \rd u
}}
{{end-eqn}}
Let $\map \phi a > \map \phi b$.
Then:
{{begin-eqn}}
{{eqn | l = \int_{\map \phi b}^{\map \phi a} \map f t \rd t
      | r = \int_{\map \phi b}^{\map \phi a} \map \Re {\map f t} \rd t + i \int_{\map \phi b}^{\map \phi a} \map \Im {\map f t} \rd t
      | c = {{Defof|Complex Riemann Integral}}
}}
{{eqn | r = -\int_a^b \map \Re {\map f {\map \phi u} } \map {\phi'} u \rd u - i \int_a^b \map \Im {\map f {\map \phi u} } \map {\phi'} u \rd u
      | c = Integration by Substitution: Definite Integral
}}
{{eqn | r = - \paren{ \int_a^b \map \Re {\map f {\map \phi u} \map {\phi'} u} \rd u + i \int_a^b \map \Im {\map f {\map \phi u} \map {\phi'} u} \rd u }
      | c = Multiplication of Real and Imaginary Parts
}}
{{eqn | r = -\int_a^b \map f {\map \phi u} \map {\phi'} u \rd u
}}
{{end-eqn}}
{{qed}}
Theorem: Continuous Injection of Interval is Strictly Monotone

Let $I$ be a real interval.
Let $f: I \to \R$ be an injective continuous real function.
Then $f$ is strictly monotone.

Proof:
{{AimForCont}} $f$ is not strictly monotone.
That is, there exist $x, y, z \in I$ with $x < y < z$ such that either:
:$\map f x \le \map f y$ and $\map f y \ge \map f z$
or:
:$\map f x \ge \map f y$ and $\map f y \le \map f z$
Suppose $\map f x \le \map f y$ and $\map f y \ge \map f z$.
If $\map f x = \map f y$, or $\map f y = \map f z$, or $\map f x = \map f z$, $f$ is not injective, which is a contradiction.
Thus, $\map f x < \map f y$ and $\map f y > \map f z$.
Suppose $\map f x < \map f z$.
That is:
:$\map f x < \map f z < \map f y$
As $f$ is continuous on $I$, the Intermediate Value Theorem can be applied.
Hence there exists $c \in \openint x y$ such that $\map f c = \map f z$.
As $z \notin \openint x y$, we have $c \ne z$.
So $f$ is not injective, which is a contradiction.
Suppose instead $\map f x > \map f z$.
That is:
:$\map f z < \map f x < \map f y$
Again, as $f$ is continuous on $I$, the Intermediate Value Theorem can be applied.
Then, there exists $c \in \openint y z$ such that $\map f c = \map f x$.
So $f$ is not injective, which is a contradiction.
If we suppose $\map f x \ge \map f y$ and $\map f y \le \map f z$, we reach a similar contradiction.
By Proof by Contradiction, $f$ is strictly monotone.
{{qed}}
Category:Continuous Functions
hxzen2o88ifwj49yejmuutk0iw47g9n
Theorem: Prime Ideal in Lattice

Let $\struct {L, \le}$ be a lattice.
Let $I$ be an ideal in $L$.
Then $I$ is a prime ideal {{iff}}:
:$\forall a, b \in L: a \wedge b \in I \implies a \in I \text{ or } b \in I$
where $a \wedge b$ denotes $\min \set {a, b}$, the meet of $a$ and $b$.

Proof:
=== Necessary Condition ===
Let $I$ be a prime ideal.
Let $a, b \in L$ such that $a, b \notin I$.
Then $a, b \in L \setminus I$.
By the definition of prime ideal $L \setminus I$ is a filter.
By the definition of a filter:
:$\exists c \in L \setminus I: c \le a, c \le b$
By the definition of meet:
:$c \le a \wedge b$
Since $c \in L \setminus I$, the definition of a filter implies that
:$a \wedge b \in L \setminus I$
{{refactor|The above argument should be extracted into a separate page which may or may not be instantiated as a separate definition of a filter. As it is, we haven't even got the definition of "meet" written yet - although whether there is any point in doing so as $a \wedge b :{{=}} \inf \set {a, b}$ should be sufficient.|level = medium}}
Thus $a \wedge b \notin I$.
By contraposition it follows that $a \wedge b \in I$ implies that $a \in I$ or $b \in I$.
{{qed|lemma}}
Theorem: Inverse of Increasing Bijection need not be Increasing

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $\phi: S \to T$ be a bijection which is increasing.
Then $\phi^{-1}: T \to S$ is not necessarily also increasing.

Proof:
Proof by Counterexample:
Let $S := \powerset {\set {a, b} }$.
Let $T := \set {1, 2, 3, 4}$.
From Subset Relation on Power Set is Partial Ordering, $\struct {S, \subseteq}$ is an ordered set.
Clearly so is $\struct {T, \le}$ (although its ordering is in fact total, it is still technically an ordered set).
Let $\phi: S \to T$ be defined as:
{{begin-eqn}}
{{eqn | l = \map \phi \O
      | r = 1
}}
{{eqn | l = \map \phi {\set a}
      | r = 2
}}
{{eqn | l = \map \phi {\set b}
      | r = 3
}}
{{eqn | l = \map \phi {\set {a, b} }
      | r = 4
}}
{{end-eqn}}
By inspection it can be seen that $\phi$ is a bijection.
Also by inspection it can be seen that $\phi$ is increasing.
But note that while $2 \le 3$, it is not the case that $\set a \subseteq \set b$.
That is, $\phi^{-1}$ is ''not'' increasing.
{{qed}}
Theorem: Order Isomorphic Sets are Equivalent

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be order isomorphic.
Then $S$ and $T$ are equivalent.

Proof:
By definition, an order isomorphism is a bijection $\phi$ such that:
:$\phi: S \to T$ is order-preserving
:$\phi^{-1}: T \to S$ is order-preserving.
So, by definition, there exists a bijection between $S$ and $T$.
The result follows by definition of set equivalence.
{{qed}}
Theorem: Linear Combination of Contour Integrals

Let $C$ be a contour in $\C$.
Let $f, g: \Img C \to \C$ be continuous complex functions, where $\Img C$ denotes the image of $C$.
Let $\lambda, \mu \in \C$ be complex constants.
Then:
:$\ds \int_C \paren {\lambda \map f z + \mu \map g z} \rd z = \lambda \int_C \map f z \rd z + \mu \int_C \map g z \rd z$

Proof:
By definition of contour, $C$ is a finite sequence $C_1, \ldots, C_n$ of directed smooth curves.
Let $C_k$ be parameterized by the smooth path $\gamma_k: \closedint {a_k} {b_k} \to \C$ for all $k \in \set {1, \ldots, n}$.
Then:
{{begin-eqn}}
{{eqn | l = \int_C \paren {\lambda \map f z + \mu \map g z} \rd z
      | r = \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \paren {\lambda \map f {\map {\gamma_k} t} + \mu \map g {\map {\gamma_k} t} } \map {\gamma_k'} t \rd t
      | c = {{Defof|Complex Contour Integral}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n \paren {\lambda \int_{a_k}^{b_k} \map f {\map {\gamma_k} t} \map {\gamma_k'} t \rd t + \mu \int_{a_k}^{b_k} \map g {\map {\gamma_k} t} \map {\gamma_k'} t \rd t}
      | c = Linear Combination of Complex Integrals
}}
{{eqn | r = \lambda \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \map f {\map {\gamma_k} t} \map {\gamma_k'} t \rd t + \mu \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \map g {\map {\gamma_k} t} \map {\gamma_k'} t \rd t
}}
{{eqn | r = \lambda \int_C \map f z \rd z + \mu \int_C \map g z \rd z 
}}
{{end-eqn}}
{{qed}}
Theorem: P-Product Metric Induces Product Topology

Let $M_A = \struct{A, d_A}$ and $M_B = \struct{B, d_B}$ be metric spaces.
Let $\tau_A$ and $\tau_B$ be the topologies on $A$ and $B$ induced by $d_A$ and $d_B$, respectively.
Let $p \ge 1$ be an extended real number.
Let $M = \struct{A \times B, d}$ be the $p$-product of $M_A$ and $M_B$.
We have that $M$ is a metric space.
Let $\tau$ be the topology on $A \times B$ induced by $d$.
Then $\struct{A \times B, \tau}$ is the product space of $\struct{A, \tau_A}$ and $\struct{B, \tau_B}$.

Proof:
By $p$-Product Metrics are Lipschitz Equivalent and Lipschitz Equivalent Metrics are Topologically Equivalent, it suffices to consider the case $p = \infty$.
Let $\struct{A \times B, \tau'}$ be the product space of $\struct{A, \tau_A}$ and $\struct{B, \tau_B}$.
By the definition of $d$, it follows that an open ball in $M$ is the (Cartesian) product of an open ball in $M_A$ and an open ball in $M_B$.
Since an open ball is an open set, it follows from Equivalence of Definitions of Analytic Basis that $\tau \subseteq \tau'$.
Let $W \in \tau'$, $\tuple {x, y} \in W$.
By the definition of $\tau'$, it follows from Equivalence of Definitions of Analytic Basis that there exists a $U$ open in $M_A$ and a $V$ open in $M_B$ such that $\tuple {x, y} \in U \times V \subseteq W$.
By the definition of an open set:
:There exists a strictly positive real number $\alpha \in \R_{>0}$ such that the open $\alpha$-ball of $x$ in $M_A$ is contained in $U$
:There exists a strictly positive real number $\beta \in \R_{>0}$ such that the open $\beta$-ball of $y$ in $M_B$ is contained in $V$
Let $\epsilon = \min \set {\alpha, \beta}$.
Then $\epsilon \in \R_{>0}$, and the open $\epsilon$-ball of $\tuple {x, y}$ in $M$ is contained in $U \times V$.
Hence, $W$ is open in $M$.
That is, $\tau' \subseteq \tau$.
By definition of set equality:
:$\tau = \tau'$
as desired.
{{qed}}