avewright/proofwiki-math huggingface dataset:
Theorem: P-Product Metrics are Lipschitz Equivalent

Let $M_A = \left({A, d_A}\right)$ and $M_B = \left({B, d_B}\right)$ be metric spaces.
Let $\tau_A$ and $\tau_B$ be the topologies on $A$ and $B$ induced by $d_A$ and $d_B$, respectively.
For all extended real numbers $p \ge 1$, let $M_p = \left({A \times B, d_p}\right)$ be the $p$-product of $M_A$ and $M_B$.
Then all the metrics $\left\{{d_p: p \ge 1}\right\}$ are Lipschitz equivalent.

Proof:
From $p$-Product Metric is Metric, $M_p$ is a metric space.
For all real numbers $p \ge 1$, it follows from the definition of $d_p$ that:
:$\forall x, y \in A \times B: d_{\infty} \left({x, y}\right) \le d_p \left({x, y}\right) \le 2^{1/p} d_{\infty} \left({x, y}\right)$
Hence, $d_p$ and $d_{\infty}$ are Lipschitz equivalent.
The result follows from Lipschitz Equivalence is Equivalence Relation.
{{qed}}
Category:Lipschitz Equivalence
Category:P-Product Metrics
e5q0v5e89hcpltsp1iq4vys99oipf9s
Theorem: Ordered Sum of Tosets is Totally Ordered Set/General Result

Let $S_1, S_2, \ldots, S_n$ all be tosets.
Let $T_n$ be the ordered sum of $S_1, S_2, \ldots, S_n$:
:$\forall n \in \N_{>0}: T_n = \begin{cases}
S_1 & : n = 1 \\
T_{n - 1} + S_n & : n > 1
\end{cases}$
Then $T_n$ is a toset.

Proof:
From Ordered Sum of Tosets is Totally Ordered Set, $S_1 + S_2$ is a toset.
Suppose $T_{n-1}$ is a toset.
Given that $S_n$ is a toset, it follows from Ordered Sum of Tosets is Totally Ordered Set that $T_{n-1} + S_n$ is also a toset.
The result follows by induction.
{{qed}}
Category:Total Orderings
Category:Ordered Sums
ef09nrsn8gjky7rbwjtm67biqpmmpxh
Theorem: Supremum of Suprema

Let $\struct {S, \preceq}$ be an ordered set.
Let $\mathbb T \subseteq \powerset S$, where $\powerset S$ is the power set of $S$.
Suppose all $T \in \mathbb T$ admit a supremum $\sup T$ in $S$.
Then:
:$\sup \bigcup \mathbb T = \sup {\set {\sup T: T \in \mathbb T} }$
if one of these two quantities exists (in $S$).

Proof:
Suppose that $s = \sup \bigcup \mathbb T \in S$.
By Set is Subset of Union, $T \subseteq \bigcup \mathbb T$ for all $T \in \mathbb T$.
Hence by Supremum of Subset:
:$\forall T \in \mathbb T: \sup T \preceq s$
Suppose now that $a \in S$ satisfies:
:$\forall T \in \mathbb T: \sup T \preceq a$
Then by transitivity of $\preceq$:
:$\forall t \in T: t \preceq a$
Since this holds for any $T \in \mathbb T$, also:
:$\forall t \in \bigcup \mathbb T: t \preceq a$
Hence $s \preceq a$, by definition of supremum.
That is, $s = \sup {\set {\sup T: T \in \mathbb T} }$.
{{qed|lemma}}
Suppose now that $r = \sup {\set {\sup T: T \in \mathbb T} } \in S$.
By definition of supremum, for all $T \in \mathbb T$ and $t \in T$:
:$t \preceq \sup T$
By transitivity of $\preceq$:
:$\forall T \in \mathbb T: \forall t \in T: t \preceq r$
Hence for all $t \in \bigcup \mathbb T$:
:$t \preceq r$
Suppose that $a \in S$ satisfies:
:$\forall t \in \bigcup \mathbb T: t \preceq a$
In particular, for any $T \in \mathbb T$, since $T \subseteq \bigcup \mathbb T$:
:$\sup T \preceq a$
and therefore by definition of supremum, also:
:$r \preceq a$
That is, $r = \sup \bigcup \mathbb T$.
{{qed}}
Category:Order Theory
2fhnbjumyyvbt8a4ykp6kutfy4l6h0w
Theorem: Antilexicographic Product of Totally Ordered Sets is Totally Ordered/General Result

Let $S_1, S_2, \ldots, S_n$ all be totally ordered sets.
Let $T_n$ be the antilexicographic product of $S_1, S_2, \ldots, S_n$:
:$\forall n \in \N_{>0}: T_n = \begin {cases}
S_1 & : n = 1 \\
T_{n - 1} \otimes^a S_n & : n > 1
\end {cases}$
Then $T_n$ is a totally ordered set.

Proof:
From Antilexicographic Product of Totally Ordered Sets is Totally Ordered, $S_1 \otimes^a S_2$ is a totally ordered set.
Suppose $T_{n - 1}$ is a totally ordered set.
Given that $S_n$ is a totally ordered set, it follows from Antilexicographic Product of Totally Ordered Sets is Totally Ordered that $T_{n - 1} \otimes^a S_n$ is also a totally ordered set.
The result follows by induction.
{{qed}}
{{finish}}
Category:Antilexicographic Product of Totally Ordered Sets is Totally Ordered
safbetit1r7fldhahlo3w9bxceouic5
Theorem: Derivative of Complex Composite Function

Let $f: D \to \C$ be a complex-differentiable function, where $D \subseteq \C$ is an open set.
Let $g: \Img f \to \C$ be a complex-differentiable function, where $\Img f$ denotes the image of $f$.
Define $h = f \circ g: D \to C$ as the composite of $f$ and $g$.
Then $h$ is complex-differentiable, and its derivative is defined as:
:$\forall z \in D: \map {h'} z =  \map {f'} {\map g z} \map {g'} z$

Proof:
{{MissingLinks|among general reference to results, maybe also some links to details on this "method of variations" approach}}
Put $y = \map g z$.
Let $\delta z \in \C \setminus \set 0$.
Put $\delta y = \map g {z + \delta z} - y$, so:
:$\map g {z + \delta z} = y + \delta y$
As $\delta z \to 0$, we have:
:$(1): \quad \delta y \to 0$ by definition of continuity, as $g$ is continuous.
:$(2): \quad \dfrac {\delta y} {\delta z} \to \map {g'} z$ by definition of complex-differentiability.
There are two cases to consider:
Theorem: Ring of Idempotents is Idempotent Ring

Let $\struct {R, +, \circ}$ be a commutative ring.
Let $\struct {A, \oplus, \circ}$ be its ring of idempotents.
Then $\struct {A, \oplus, \circ}$ is an idempotent ring.

Proof:
First, it is to be established that $\struct {A, \oplus, \circ}$ is a ring in the first place.
This we do by verifying the ring axioms.
Theorem: Reparameterization of Contour is Contour

Let $\closedint a b$ and $\closedint c d$ be closed real intervals.
Let $\gamma: \closedint a b \to \C$ be a contour in $\C$.
That is, there exists a subdivision $a_0, a_1 , \ldots, a_n$ of $\closedint a b$ such that $\gamma \restriction_{I_i}$ is a smooth path for all $i \in \set {1, \ldots, n}$, where $I_i = \closedint {a_{i - 1} } {a_i}$.
Here, $\gamma \restriction_{I_i}$ denotes the restriction of $\gamma$ to $I_i$.
Let $\phi: \closedint c d \to \closedint a b$  be a differentiable real function with $\map \phi c = a$, and $\map \phi d = b$.
Suppose that $\phi$ is either bijective or strictly increasing.
Define $\sigma: \closedint c d \to \C$ as a composite function by $\sigma = \gamma \circ \phi$.
Then $\sigma$ is a contour.
For all $i \in \set {1, \ldots, n}$, let $J_i := \closedint {\map {\phi^{-1} } {a_{i - 1} } } {\map {\phi^{-1} } {a_i} }$.
Then:
:$\map {\sigma' \restriction_{J_i} } t = \map {\gamma' \restriction_{I_i} } {\map \phi t} \map {\phi'} t$

Proof:
$\phi$ is either bijective or strictly increasing.
From Continuous Real Function on Closed Interval is Bijective iff Strictly Monotone, it follows that in both cases $\phi$ is both bijective and strictly monotone.
As $\map \phi c < \map \phi d$, $\phi$ must be strictly increasing.
As $\phi$ is strictly increasing, we have $c = \map {\phi^{-1} } {a_0} < \map {\phi^{-1} } {a_1} < \cdots < \map {\phi^{-1} } {a_n} = d$.
Hence, $\map {\phi^{-1} } {a_0}, \map {\phi^{-1} } {a_1}, \dotsc, \map {\phi^{-1} } {a_n}$ form a subdivision of $\closedint a b$.
Define $J_i := \closedint {\map {\phi^{-1} } {a_{i - 1} } } {\map {\phi^{-1} } {a_i} }$ as a closed real interval.
From Derivative of Complex Composite Function, it follows that $\sigma$ restricted to $J_i$ is complex differentiable.
Its derivative is given by:
:$\map {\sigma' \restriction_{J_i} } t = \map {\gamma' \restriction_{I_i} } {\map \phi t} \map {\phi'} t$
From Derivative of Monotone Function, it follows that for all $t \in \closedint c d$, we have $\map {\phi'} t > 0$.
As $\map {\gamma' \restriction_{I_i} } {\map \phi t} \ne 0$ by definition of contour, we have $\map {\sigma' \restriction_{J_i} } t \ne 0$.
Then $\sigma$ fulfils both requirement $(1)$ and $(2)$ from the definition of contour, so $\sigma$ is a contour.
{{qed}}
Theorem: Contour Integral is Independent of Parameterization

Let $C$ be a contour defined by 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}$.
Let $f: \Img C \to \C$ be a continuous complex function, where $\Img C$ denotes the image of $C$.
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 \int_C \map f z \rd z = \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$

Proof:
By definition of parameterization:
:$\gamma_k = \sigma_k \circ \phi_i$
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 real function.
Then:
{{begin-eqn}}
{{eqn | l = \int_C \map f z \rd z 
      | r = \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \map f {\map {\gamma_k} t} \map {\gamma_k'} t \rd t
      | c = {{Defof|Complex Contour Integral}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n \int_{\map {\phi_k^{-1} } {a_k} }^{\map {\phi_k^{-1} } {b_k} } \map f {\map {\gamma_k} {\map {\phi_k} u} } \map {\gamma_k'} {\map {\phi_k} u} \map {\phi_k'} u \rd u
      | c = substitution with $t = \map {\phi_k} u$
}}
{{eqn | r = \sum_{k \mathop = 1}^n \int_{\map {\phi_k^{-1} } {a_k} }^{\map {\phi_k^{-1} } {b_k} } \map f {\map {\sigma_k} u} \map {\sigma_k'} u \rd u
      | c = Derivative of Complex Composite Function
}}
{{eqn | r = \sum_{k \mathop = 1}^n \int_{c_k}^{d_k} \map f {\map {\sigma_k} u} \map {\sigma_k'} u \rd u
      | c = Reparameterization of Directed Smooth Curve Maps Endpoints To Endpoints
}}
{{end-eqn}}
{{qed}}
Theorem: Unity is Unity in Ring of Idempotents

Let $\left({R, +, \circ}\right)$ be a commutative and unitary ring whose unity is $1_R$.
Let $\left({A, \oplus, \circ}\right)$ be the ring of idempotents of $R$.
Then $1_R$ is also a unity for $\left({A, \oplus, \circ}\right)$.

Proof:
From Unity of Ring is Idempotent, $1_R$ is an idempotent element of $R$.
Hence $1_R \in A$.
Recall that the ring product of $A$ is a restriction from that of $R$.
Hence, for each $x \in A$:
:$x \circ 1_R = x = 1_R \circ x$
so that $1_R$ is a unity for $A$, as desired.
{{qed}}
Category:Ring Theory
nspjhifbhflpwipy9lij3cnpga97hy1
Theorem: Ring of Idempotents of Commutative and Unitary Ring is Boolean Ring

Let $\struct {R, +, \circ}$ be a commutative and unitary ring.
Let $\struct {A, \oplus, \circ}$ be its ring of idempotents.
Then $\struct {A, \oplus, \circ}$ is a Boolean ring.

Proof:
From Ring of Idempotents is Idempotent Ring, $\struct {A, \oplus, \circ}$ is an idempotent ring.
By Unity is Unity in Ring of Idempotents, $\struct {A, \oplus, \circ}$ is also a unitary ring.
Hence, by definition, $\struct {A, \oplus, \circ}$ is a Boolean ring.
{{qed}}
Theorem: Boolean Ring has Proper Zero Divisor

Let $\left({R, +, \circ}\right)$ be a Boolean ring whose zero is $0_R$.
Suppose that $R$ has more than two elements.
Then $R$ has a proper zero divisor.

Proof:
Since $R$ has more than two elements, there exist distinct non-zero elements $x, y \in R$.
Note that $x + y \ne 0_R$ since $x$ and $y$ are distinct (by Idempotent Ring has Characteristic Two).
If $x \circ y = 0$, $x$ is a proper zero divisor.
If $x \circ y \ne 0$, then:
{{begin-eqn}}
{{eqn|l = \left({x \circ y}\right) \circ \left({x + y}\right)
     |r = x \circ y \circ x + x \circ y \circ y
}}
{{eqn|r = x \circ y + x \circ y
     |c = $R$ is an idempotent ring, Idempotent Ring is Commutative
}}
{{eqn|r = 0_R
     |c = Idempotent Ring has Characteristic Two
}}
{{end-eqn}}
Hence $x \circ y$ is a proper zero divisor.
The result follows, from Proof by Cases.
{{qed}}
Theorem: Continuous Real Function on Closed Interval is Bijective iff Strictly Monotone

Let $\closedint a b$ and $\closedint c d$ be closed real intervals.
Let $f: \closedint c d \to \closedint a b$ be a continuous real function.
Let $\map f c, \map f d \in \set {a, b}$.
Then $f$ is bijective {{iff}} $f$ is strictly monotone.

Proof:
=== Necessary condition ===
Let $f$ be a bijection.
From Continuous Injection of Interval is Strictly Monotone, it follows that $f$ is strictly monotone.
{{qed|lemma}}
Theorem: Concatenation of Contours is Contour

Let $C$ and $D$ be contours in the complex plane.
That is, $C$ is a finite sequence of directed smooth curves $C_1, \ldots, C_n$.
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}$.
Similarly, $D$ is a finite sequence of directed smooth curves $D_1, \ldots, D_m$.
Let $D_j$ be parameterized by the smooth path $\sigma_j: \closedint {c_j} {d_j} \to \C$ for all $j \in \set {1, \ldots, m}$.
Suppose $\map {\gamma_n} {b_n} = \map {\sigma_1} {c_1}$.
Then the finite sequence:
:$C_1, \ldots, C_n, D_1, \ldots, D_m$
defines a contour.

Proof:
By definition of contour, each $C_k$ and $D_j$ is a directed smooth curve for all $k \in \set {1, \ldots, n}, j \in \set {1, \ldots, m}$.
By definition of contour:
:$\map {\gamma_k} {b_k} = \map {\gamma_{k + 1} } {a_{k + 1} }$
and:
:$\map {\sigma_j} {d_j} = \map {\sigma_{j + 1} } {c_{j + 1} }$
for all $k \in \set {1, \ldots, n - 1}$ and $j \in \set {1, \ldots, m - 1}$.
By assumption:
:$\map {\gamma_n} {b_n} = \map {\sigma_1} {c_1}$
Hence, $C_1, \ldots, C_n, D_1, \ldots, D_m$ defines a contour.
{{qed}}
Theorem: Contour Integral of Concatenation of Contours

Let $C$ and $D$ be contours in $\C$.
Suppose that the end point of $C$ is equal to the start point of $D$, so the concatenation $C \cup D$ is defined.
Let $f: \Img {C \cup D} \to \C$ be a continuous complex function, where $\Img {C \cup D}$ denotes the image of $C \cup D$.
Then:
:$\ds \int \limits_{C \mathop \cup D} \map f z \rd z = \int \limits_C \map f z \rd z + \int \limits_D \map f 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}$.
Similarly, $D$ is a finite sequence $D_1, \ldots, D_m$ of directed smooth curves.
Let $D_j$ be parameterized by the smooth path $\sigma_j: \closedint {c_j} {d_j} \to \C$ for all $j \in \set {1, \ldots, m}$.
Put $\gamma_k = \sigma_{k - n}, a_k = c_{k - n}$ and $b_k = d_{k - n}$ for all $k \in \set {n + 1, \ldots, n + m}$.
Then $C \cup D$ is a sequence of $n + m$ directed smooth curves which are parameterized by $\gamma_1, \ldots, \gamma_{n + m}$.
Then:
{{begin-eqn}}
{{eqn | l = \int \limits_{C \mathop \cup D} \map f z \rd z
      | r = \sum_{k \mathop = 1}^{n + m} \int_{a_k}^{b_k} \map f {\map {\gamma_k} t} \map {\gamma_k'} t \rd t
      | c = {{Defof|Complex Contour Integral}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \map f {\map {\gamma_k} t} \map {\gamma_k'} t \rd t + \sum_{j \mathop = 1}^m \int_{c_j}^{d_j} \map f {\map {\sigma_j} t} \map {\sigma_j'} t \rd t
}}
{{eqn | r = \int \limits_C \map f z \rd z + \int \limits_D \map f z \rd z
      | c = {{Defof|Complex Contour Integral}}
}}
{{end-eqn}}
{{qed}}
Theorem: Regular Expression is Accepted by Finite State Machine

Let $R$ be a regular expression.
Then there exists a finite state machine $F$ such that its accepted language $\map L F$ is exactly $\map L R$, the language defined by $R$.

Proof:
This proof proceeds by structural induction.
Theorem: Directed Smooth Curve Relation is Equivalence

Let $\sim$ denote a relation on the set of all smooth paths: $\set {\gamma: I \to \C : \text{$I$ is a closed real interval, $\gamma$ is a smooth path} }$.
Let $\gamma: \closedint a b \to \C$ and $\sigma : \closedint c d \to \C$ be smooth paths.
Define $\sim$ as follows: 
:$\gamma \sim \sigma$ {{iff}} there exists a bijective differentiable strictly increasing real function $\phi: \closedint c d \to \closedint a b$ such that $\sigma = \gamma \circ \phi$.
Then $\sim$ is an equivalence relation on the set of all smooth paths.

Proof:
Checking in turn each of the criteria for an equivalence:
Theorem: Reparameterization of Directed Smooth Curve Preserves Image

Let $\closedint a b$ and $\closedint c d$ be closed real intervals.
Let $\gamma : \closedint a b \to \C$ be a smooth path.
Let $C$ be a directed smooth curve with parameterization $\gamma$.
Suppose that $\sigma : \closedint c d \to \C$ is a reparameterization of $C$.
Then $\Img \gamma = \Img \sigma$, where $\Img \gamma$ denotes the image of $\gamma$.

Proof:
By definition of directed smooth curve, there exists a bijective differentiable strictly increasing function $\phi: \closedint c d \to \closedint a b$ such that $\sigma = \gamma \circ \phi$.
From Surjection by Restriction of Codomain, it follows that there exists a function $\tilde \gamma: \closedint a b \to \Img \gamma$ that is the surjective restriction of $\gamma$ to $\Img \gamma$.
Put $\tilde \sigma := \tilde \gamma \circ \phi : \closedint c d \to \Img \gamma$.
From Composite of Surjections is Surjection, it follows that $\tilde \sigma$ is surjective.
Then:
:$\Img {\tilde \sigma} = \Img \gamma$
Now:
:$\map \sigma t = \map {\tilde \sigma} t$ for all $t \in \closedint c d = \Dom \sigma = \Dom {\tilde \sigma}$
where $\Dom \sigma$ denotes the domain of $\sigma$.
It follows that:
:$\Img \sigma = \Img {\tilde \sigma}$
Hence:
:$\Img {\tilde \gamma} = \Img \sigma$
{{qed}}
Theorem: Reparameterization of Directed Smooth Curve Maps Endpoints To Endpoints

Let $\R^n$ be a real cartesian space of $n$ dimensions.
Let $\closedint a b$ and $\closedint c d$ be closed real intervals.
Let $\gamma: \closedint a b \to \R^n$ be a smooth path in $\R^n$.
Let $C$ be a directed smooth curve with parameterization $\gamma$.
Suppose that $\sigma: \closedint c d \to \R^n$ is a reparameterization of $C$.
Then the start points and end points of $\gamma$ and $\sigma$ are identical:
:$\map \gamma a = \map \sigma c$
:$\map \gamma b = \map \sigma d$

Proof:
By definition of reparameterization, there exists a bijective differentiable strictly increasing real function $\phi: \closedint c d \closedint a b$ such that $\sigma = \gamma \circ \phi$.
As $\map {\phi^{-1} }{a} \in \closedint c d$:
: $c \le \map {\phi^{-1} }{a}$
As $\phi$ is strictly increasing:
: $\map \phi c \le \map \phi { \map {\phi^{-1} } a } = a$
As $\map \phi c \in \closedint a b$:
:$\map \phi c = a$
Hence:
:$\map \sigma c = \map {\gamma \circ \phi} c = \map \gamma a$
As $\map {\phi^{-1} } b \in \closedint c d$:
: $d \ge \map {\phi^{-1} } b$
As $\phi$ is strictly increasing:
: $\map \phi d \ge \map \phi { \map {\phi^{-1} } b } = b$
As $\map \phi d \in \closedint a b$:
: $\map \phi d = b$
Hence:
:$\map \sigma d = \map {\gamma \circ \phi} d = \map \gamma b)$
{{qed}}
Theorem: Product of Ring Negatives

Let $\struct {R, +, \circ}$ be a ring.
Then:
:$\forall x, y \in \struct {R, +, \circ}: \paren {-x} \circ \paren {-y} = x \circ y$
where $\paren {-x}$ denotes the negative of $x$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \paren {-x} \circ \paren {-y}
      | r = -\paren {x \circ \paren {-y} }
      | c = Product with Ring Negative
}}
{{eqn | r = -\paren {-\paren {x \circ y} }
      | c = Product with Ring Negative
}}
{{eqn | r = x \circ y
      | c = Negative of Ring Negative
}}
{{end-eqn}}
{{qed}}
Theorem: Metric for Distinct Elements in Metric Space is Strictly Positive

Let $A$ be a set.
Let $d: A \times A \to \R$ be a real-valued function on $A$ with the following properties:
{{begin-axiom}}
{{axiom | n = \text M 1'
        | q = \forall x, y \in A
        | m = \map d {x, y} = 0 \iff x = y
}}
{{axiom | n = \text M 2
        | q = \forall x, y, z \in A
        | m = \map d {x, y} + \map d {y, z} \ge \map d {x, z}
}}
{{axiom | n = \text M 3
        | q = \forall x, y \in A
        | m = \map d {x, y} = \map d {y, x}
}}
{{end-axiom}}
which can be considered as being an alternative formulation of the metric space axioms.
Then:
:$\forall x, y \in A: x \ne y \implies \map d {x, y} > 0$
which is {{Metric-space-axiom|4}}.
Thus $d$ is a metric, so making $M := \struct {A, d}$ a metric space.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x, y \in A
      | l = \map d {x, y} + \map d {y, x}
      | o = \ge
      | r = \map d {x, x}
      | c = from {{Metric-space-axiom|2}}
}}
{{eqn | ll= \leadsto
      | l = 2 \map d {x, y}
      | o = \ge
      | r = 0
      | c = from Axiom $(\text M 1')$ above and {{Metric-space-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = \map d {x, y}
      | o = \ge
      | r = 0
}}
{{end-eqn}}
{{qed}}
Category:Metrics
Category:Metric Spaces
rf2gm8xug098z375zycm67r7zghbqei
Theorem: Transpose of Upper Triangular Matrix is Lower Triangular

The transpose of an upper triangular matrix is a lower triangular matrix.

Proof:
Let $\mathbf U = \sqbrk a_{m n}$ be an upper triangular matrix.
By definition:
:$\forall a_{i j} \in \mathbf U: i > j \implies a_{i j} = 0$
Let $\mathbf U^\intercal = \sqbrk b_{n m}$ be the transpose of $\mathbf U$.
That is:
:$\mathbf U^\intercal = \sqbrk b_{n m}: \forall i \in \closedint 1 n, j \in \closedint 1 n: b_{i j} = a_{j i}$
Thus:
:$\forall b_{j i} \in \mathbf U^\intercal: i > j \implies b_{j i} = 0$
By exchanging $i$ and $j$ in the notation of the above:
:$\forall b_{i j} \in \mathbf U^\intercal: i < j \implies b_{i j} = 0$
Thus by definition it is seen that $\mathbf U^\intercal$ is a lower triangular matrix.
{{qed}}
Category:Triangular Matrices
Category:Upper Triangular Matrices
Category:Lower Triangular Matrices
Category:Transposes of Matrices
mpp63usy3lpkwkgvrsx7619ff06t017
Theorem: Derivative iff Right and Left Derivative

Let $f$ be a real function.
Then $f$ is differentiable {{iff}} it has both right- and left-hand derivatives which agree.

Proof:
Derivatives are defined in terms of limits.
The result follows from Limit iff Limits from Left and Right.
{{qed}}
Theorem: Composition of Ring Homomorphisms is Ring Homomorphism

Let:
:$\struct {R_1, +_1, \odot_1}$
:$\struct {R_2, +_2, \odot_2}$
:$\struct {R_3, +_3, \odot_3}$
be rings.
Let:
:$\phi: \struct {R_1, +_1, \odot_1} \to \struct {R_2, +_2, \odot_2}$
:$\psi: \struct {R_2, +_2, \odot_2} \to \struct {R_3, +_3, \odot_3}$
be homomorphisms.
Then the composite of $\phi$ and $\psi$ is also a homomorphism.

Proof:
A specific instance of Composite of Homomorphisms on Algebraic Structure is Homomorphism.
{{qed}}