avewright/proofwiki-math huggingface dataset:
Theorem: Condition for Vectors to have Same Syndrome

Let $C$ be a linear $\tuple {n, k}$-code whose master code is $\map V {n, p}$
Let $G$ be a (standard) generator matrix for $C$.
Let $P$ be a standard parity check matrix for $C$.
Let $u, v \in \map V {n, p}$.
Then $u$ and $v$ have the same syndrome {{iff}} they are in the same coset of $C$.

Proof:
Let $u, v \in \map V {n, p}$.
Let $\map S u$ denote the syndrome of $u$.
Then:
{{begin-eqn}}
{{eqn | l = \map S u
      | r = \map S v
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = P u^\intercal
      | r = P v^\intercal
      | c = {{Defof|Syndrome}}
}}
{{eqn | ll= \leadstoandfrom
      | l = P \paren {u^\intercal - v^\intercal}
      | r = \mathbf 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = P \paren {u - v}^\intercal
      | r = \mathbf 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = u - v
      | o = \in
      | r = C
      | c = Syndrome is Zero iff Vector is Codeword
}}
{{end-eqn}}
Hence the result from Elements in Same Coset iff Product with Inverse in Subgroup.
{{qed}}
Theorem: Euler's Equation/Independent of x

Let $y$ be a mapping.
Let $J$ be a functional such that:
:$\ds J \sqbrk y = \int_a^b \map F {y, y'} \rd x$
Then the corresponding Euler's Equation can be reduced to:
:$F - y' F_{y'} = C$ 
where $C$ is an arbitrary constant.

Proof:
Assume that:
:$\ds J \sqbrk y = \int_a^b \map F {y, y'} \rd x$
Then:
{{begin-eqn}}
{{eqn| l = \delta J
     | r = 0
}}
{{eqn| ll= \leadsto
     | l = F_y - \dfrac \d {\d x} F_{y'}
     | r = F_y - \paren {\dfrac {\d y} {\d x} \dfrac {\partial F_{y'} } {\partial y} + \dfrac {\d y'} {\d x} \dfrac {\partial F_{y'} } {\partial y'} }
}}
{{eqn| r = F_y - y' F_{y'y} - y'' F_{y'y'}
}}
{{end-eqn}}
Multiply this differential equation by $y'$.
This gives:
{{begin-eqn}}
{{eqn | l = F_y y' - {y'}^2 F_{y'y} - y'y'' F_{y'y'}
      | r = \paren {F_{y} y' + F_{y'} y''} - F_{y'} y'' - y' \paren {y' F_{y'y} + y'' F_{y'y'} }
}}
{{eqn | r = \dfrac {\d F} {\d x} - y' \paren {\dfrac {\d y} {\d x} \dfrac {\partial F_{y'} } {\partial y} + \dfrac {\d y'} {\d x} \dfrac {\partial F_{y'} } {\partial y'} } - F_{y'} y''
}}
{{eqn | r = \dfrac {\d F} {\d x} - y' \dfrac {\d F} {\d x} - \dfrac {\d y'} {\d x} F_{y'}
}}
{{eqn | r = \dfrac \d {\d x} \paren {F - y' F_{y'} }
}}
{{eqn | r = 0
}}
{{end-eqn}}
Integration yields the desired result.
{{qed}}
Theorem: Euler's Equation/Independent of y

Let $y$ be a mapping
Let $J$ be a functional such that
:$\ds J \sqbrk y = \int_a^b \map F {x,y'} \rd x$
Then the corresponding Euler's equation can be reduced to:
:$F_{y'} = C$ 
where $C$ is an arbitrary constant.

Proof:
Assume that:
:$\ds J \sqbrk y = \int_a^b \map F {x,y'} \rd x$
Euler's equation for $J$ is:
:$\dfrac \d {\d x} F_{y'} = 0$
Integration yields:
:$F_{y'} = C$ 
{{qed}}
Theorem: Euler's Equation/Independent of y'

Let $y$ be a mapping.
Let $J$ a functional be such that
:$\ds J \sqbrk y = \int_a^b \map F {x,y} \rd x$
Then the corresponding Euler's Equation can be reduced to:
:$F_y = 0$ 
Furthermore, this is an algebraic equation.

Proof:
Assume that:
:$\ds J \sqbrk y = \int_a^b \map F {x,y} \rd x$
Then Euler's Equation for $J$ is:
:$F_y = 0$
Since $F$ is independent of $y'$, the equation is algebraic.
{{qed}}
Theorem: Euler's Equation/Integrated wrt Length Element

Let $y$ be a real mapping belonging to $C^2$ differentiability class.
Assume that:
:$\ds J \sqbrk y = \int_a^b \map f {x, y, y'} \rd s$
where
:$\rd s = \sqrt {1 + y'^2} \rd x$
Then Euler's Equation can be reduced to:
:$f_y - f_x y' - f_{y'} y' y' ' - f \dfrac {y' '} {\paren {1 + y'^2}^{\frac 3 2} } = 0$

Proof:
Substitution of $\rd s$ into $J$ results in the following functional:
:$\ds J \sqbrk y = \int_a^b \map f {x, y, y'} \sqrt {1 + y'^2} \rd x$
We can consider this as a functional with the following effective $F$:
:$F = \map f {x, y, y'} \sqrt {1 + y'^2}$
Find Euler's Equation:
{{begin-eqn}}
{{eqn | l = F_y - \dfrac \d {\d x} F_{y'}
      | r = f_y \sqrt {1 + y'^2} - \dfrac \d {\d x} \paren {\map f {x, y, y'} \frac {y'} {\sqrt {1 + y'^2} } }
}}
{{eqn | r = f_y \sqrt {1 + y'^2} - \dfrac \d {\d x} \map f {x, y, y'} \frac {y'} {\sqrt {1 + y'^2} } - \map f {x, y, y'} \dfrac \d {\d x} \frac {y'} {\sqrt {1 + y'^2} }
}}
{{eqn | r = f_y \sqrt {1 + y'^2} - f_x \frac {y'} {\sqrt {1 + y'^2} } - f_y \frac {y'^2} {\sqrt {1 + y'^2} } - f_{y'} \frac {y' y' '} {\sqrt {1 + y'^2} } - f \frac {y' ' \sqrt {1 + y'^2} - \frac {y'^2 y' '} {\sqrt {1 + y'^2} } } {1 + y'^2}
}}
{{eqn | r = \frac 1 {\sqrt {1 + y'^2} } \paren {f_y - f_x y' - f_{y'} y' y' ' - f \frac {y' '} {\paren {1 + y'^2}^{\frac 3 2} } }
}}
{{end-eqn}}
Due to assumptions on $y$, the prefactor does not vanish.
By Euler's Equation, the last expression vanishes.
{{qed}}
Theorem: Subset of Linear Code with Even Weight Codewords

Let $C$ be a linear code.
Let $C^+$ be the subset of $C$ consisting of all the codewords of $C$ which have even weight.
Then $C^+$ is a subgroup of $C$ such that either $C^+ = C$ or such that $\order {C^+} = \dfrac {\order C} 2$.

Proof:
Note that the zero codeword is in $C^+$ as it has a weight of $0$ which is even.
Let $c$ and $d$ be of even weight, where $c$ and $d$ agree in $k$ ordinates.
Let $\map w c$ denote the weight of $c$.
Then:
{{begin-eqn}}
{{eqn | l = \map w {c + d}
      | r = \map w c - k + \map w d - k
      | c = 
}}
{{eqn | r = \map w c + \map w d - 2 k
      | c = 
}}
{{end-eqn}}
which is even.
Since the negative of a vector $\mathbf v$ in $\Z_2$ equals $\mathbf v$, it follows that the inverse of $c \in C$ is also in $C$.
It follows from the Two-Step Subgroup Test that $C^+$ is a subgroup of $C$.
Let $C \ne C^+$.
Then $C$ contains a codeword $c$ of odd weight.
Let $C^-$ denote the subset of $C$ consisting of all the codewords of $C$ which have odd weight.
Adding $c$ to each codeword of $C^+$ gives distinct codewords of odd weight, so:
:$\order {C^-} \ge \order {C^+}$
Similarly, adding $c$ to each codeword of $C^-$ gives distinct codewords of even weight, so:
:$\order {C^-} \le \order {C^+}$
As $C = C^+ \cup C^-$ it follows that:
:$\order C = 2 \order {C^+}$
Hence the result.
{{qed}}
Theorem: Minimal Smooth Surface of Revolution

Let $\map y x$ be a real mapping in 2-dimensional real Euclidean space.
Let $y$ pass through the points $\tuple {x_0, y_0}$ and $\tuple {x_1, y_1}$.
Consider a surface of revolution constructed by rotating $y$ around the $x$-axis.
Suppose this surface is smooth for any $x$ between $x_0$ and $x_1$.
Then its surface area is minimized by the following curve, known as a catenoid:
:$y = C \map \cosh {\dfrac {x + C_1} C}$
Furthermore, its area is:
:$A = \paren {x_1 - x_0} C \pi + \dfrac {\pi C^2} 2 \paren {\map \sinh {\dfrac {2 \paren {x_1 + C_1} } C} - \map \sinh {\dfrac {2 \paren {x_0 + C_1} } C} }$

Proof:
The area functional of the surface of revolution is:
:$\ds A \sqbrk y = 2 \pi \int_{x_0}^{x_1} y \sqrt {1 + y'^2} \rd x$
The integrand does not depend on $x$.
By Euler's Equation:
:$F - y' F_{y'} = C$
that is:
:$y \sqrt {1 + y'^2} - \dfrac {y y'^2} {\sqrt {1 + y'^2} } = C$
which is equivalent to:
:$y = C \sqrt {1 + y'^2}$
Solving for $y'$ yields:
:$y' = \sqrt {\dfrac {y^2 - C^2} {C^2} }$
Consider this as a differential equation for $\map x y$:
{{Explain|What is the definition of $\map x y$? What is the domain and what is the codomain?}}
:$\dfrac {\d x} {\d y} = \dfrac C {\sqrt {y^2 - C^2} }$
Integrate this once:
:$x + C_1 = C \ln {\dfrac {y + \sqrt {y^2 - C^2} } C}$
{{Explain|Under what conditions is this expression well defined?}}
Solving for $y$ results in:
:$y = C \cosh {\dfrac {x + C_1} C}$
To find the area, substitute this function into the formula for the area:
{{begin-eqn}}
{{eqn| l = A \sqbrk y
     | r = 2 \pi \int_{x_0}^{x_1} y \sqrt {1 + y'^2} \rd x
}}
{{eqn| r = 2 \pi \int_{x_0}^{x_1} C \, \map {\cosh^2} {\frac {x + C_1} C} \rd x
}}
{{eqn| r = \paren {x_1 - x_0} C \pi + \frac {\pi C^2} 2 \paren {\map \sinh {\frac {2 \paren {x_1 + C_1} } C} - \map \sinh {\frac {2 \paren {x_0 + C_1} } C} }
}}
{{end-eqn}}
{{Finish|Connect this to the fact that this does not always minimizes the area}}
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Open Unit Ball Equivalent implies Norm is Power of Other Norm/Lemma 2

:$\forall x \in R: \norm x_1 = \norm x_2^\alpha$

Proof:
Since $\norm {x_0}_1 < 1$ then $\norm {x_0}_2 < 1$ and:
:$\log \norm {x_0}_1 < 0$
:$\log \norm {x_0}_2 < 0$
Hence $\alpha > 0$
Since $\forall x \in R: \norm x_1 < 1 \iff \norm x_2 < 1$:
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Open Unit Ball Equivalent implies Norm is Power of Other Norm/Lemma 2/Lemma 2.1

Then:
:$\forall y \in R: \norm y_1 > 1 \iff \norm y_2 > 1$

Proof:
For $y \in R$ then:
{{begin-eqn}}
{{eqn | l = \norm y_1 > 1
      | r = \dfrac 1 {\norm y_1 } < 1
      | o = \leadstoandfrom
      | c = 
}}
{{eqn | r = \norm {y^{-1} }_1 < 1 
      | o = \leadstoandfrom
      | c = Norm of Inverse in Division Ring
}}
{{eqn | r = \norm {y^{-1} }_2 < 1 
      | o = \leadstoandfrom
      | c = by assumption
}}
{{eqn | r = \dfrac 1 {\norm y_2 } < 1
      | o = \leadstoandfrom
      | c = Norm of Inverse in Division Ring
}}
{{eqn | r = \norm y_2 > 1
      | o = \leadstoandfrom
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Equivalence of Definitions of Equivalent Division Ring Norms
7c3kw7jre137tryfpo9a96n979a9bxq
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Open Unit Ball Equivalent implies Norm is Power of Other Norm/Lemma 2/Lemma 2.2

Then:
:$\forall y \in R:\norm y_1 = 1 \iff \norm y_2 = 1$

Proof:
By assumption:
:$\forall y \in R:\norm y_1 \ge 1 \iff \norm y_2 \ge 1$
By Lemma 1:
:$\forall y \in R:\norm y_1 \le 1 \iff \norm y_2 \le 1$
Hence $\forall y \in R$:
{{begin-eqn}}
{{eqn | l = \norm y_1 = 1 
      | o = \leadstoandfrom
      | r = \norm y_1 \le 1, \norm y_1 \ge 1
}}
{{eqn | o = \leadstoandfrom
      | r = \norm y_2 \le 1, \norm y_2 \ge 1
      | c = Lemma 1 and by assumption
}}
{{eqn | o = \leadstoandfrom
      | r = \norm y_2 = 1
}}
{{end-eqn}} 
{{qed}}
Category:Equivalence of Definitions of Equivalent Division Ring Norms
i3p50dq69v4rnr033jf1x68v04xmtjz
Theorem: Symmetric Group on 3 Letters is Isomorphic to Dihedral Group D3

Let $S_3$ denote the Symmetric Group on 3 Letters.
Let $D_3$ denote the dihedral group $D_3$.
Then $S_3$ is isomorphic to $D_3$.

Proof:
Consider $S_3$ as presented by its Cayley table:
{{:Symmetric Group on 3 Letters/Cayley Table}}
Consider $D_3$ as presented by its group presentation:
{{:Group Presentation of Dihedral Group D3}}
and its Cayley table:
{{:Dihedral Group D3/Cayley Table}}
Let $\phi: S_3 \to D_3$ be specified as:
{{begin-eqn}}
{{eqn | l = \map \phi {1 2 3}
      | r = a
      | c = 
}}
{{eqn | l = \map \phi {2 3}
      | r = b
      | c = 
}}
{{end-eqn}}
Then by inspection, we see:
{{begin-eqn}}
{{eqn | l = \map \phi {1 3 2}
      | r = a^2
      | c = 
}}
{{eqn | l = \map \phi {1 3}
      | r = a b
      | c = 
}}
{{eqn | l = \map \phi {1 2}
      | r = a^2 b
      | c = 
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Homomorphism from Group of Cube Roots of Unity to Itself

Let $\struct {U_3, \times}$ denote the multiplicative group of the complex cube roots of unity.
Here, $U_3 = \set {1, \omega, \omega^2}$ where $\omega = e^{2 i \pi / 3}$.
Let $\phi: U_3 \to U_3$ be defined as:
:$\forall z \in U_3: \map \phi z = \begin{cases} 1 & : z = 1 \\ \omega^2 & : z = \omega \\ \omega & : z = \omega^2 \end{cases}$
Then $\phi$ is a group homomorphism.

Proof:
It is noted that
:$\paren {\omega^2}^2 = \omega$
and so $\phi$ is the square function.
By Roots of Unity under Multiplication form Cyclic Group and Cyclic Group is Abelian, $U_3$ is abelian.
Thus for all $a, b \in U_3$:
{{begin-eqn}}
{{eqn | l = \map \phi a \map \phi b
      | r = a^2 b^2
}}
{{eqn | r = a b a b
      | c = {{Defof|Abelian Group}}
}}
{{eqn | r = \paren {a b}^2
}}
{{eqn | r = \map \phi {a b}
}}
{{end-eqn}}
showing that $\phi$ is a group homomorphism.
{{qed}}
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Open Unit Ball Equivalent implies Norm is Power of Other Norm/Lemma 2/Lemma 2.3

:$\alpha = \beta$

Proof:
Because $x, y \in R \setminus 0_R$:
:$\norm x_1 , \norm y_1, \norm x_2 , \norm y_2 > 0$.
Because $\norm{x}_1 , \norm {y}_1 \ne 1$, by Lemma 2:
:$\norm x_2 , \norm y_2 \ne 1$.
Hence:
:$\log \norm x_1 , \log \norm y_1, \log \norm x_2, \log \norm y_2 \ne 0$ 
and $\alpha, \beta$ are well-defined.
Let $r = \dfrac n m \in \Q$ be any rational number where $n, m \in \Z$ are integers and $m \ne 0$.
Then:
{{begin-eqn}}
{{eqn | l = \norm y_1^n < \norm x_1^m
      | o = \leadstoandfrom
      | r = \dfrac {\norm y_1^n} {\norm x_1^m} < 1
}}
{{eqn | o = \leadstoandfrom
      | r = \norm y_1^n \norm {x^{-1} }_1^m
      | c = Norm of Inverse in Division Ring
}}
{{eqn | o = \leadstoandfrom
      | r = \norm {y^n}_1 \norm {\paren {x^{-1} }^m}_1 < 1 
      | c = Norm Axiom $(\text N 2)$: Multiplicativity
}}
{{eqn | o = \leadstoandfrom
      | r = \norm {y^n \paren {x^{-1} }^m}_1 < 1 
      | c = Norm Axiom $(\text N 2)$: Multiplicativity
}}
{{eqn | o = \leadstoandfrom
      | r = \norm {y^n \paren {x^{-1} }^m}_2 < 1 
      | c = By assumption
}}
{{eqn | o = \leadstoandfrom
      | r = \norm {y^n}_2 \norm {\paren {x^{-1} }^m}_2 < 1 
      | c = Norm Axiom $(\text N 2)$: Multiplicativity
}}
{{eqn | o = \leadstoandfrom
      | r = \norm y_2^n \norm {x^{-1} }_2^m
      | c = Norm Axiom $(\text N 2)$: Multiplicativity
}}
{{eqn | o = \leadstoandfrom
      | r = \dfrac {\norm y_2^n} {\norm x_2^m} < 1
      | c = Norm of Inverse in Division Ring
}}
{{eqn | r = \norm y_2^n < \norm x_2^m
      | o = \leadstoandfrom
}}
{{end-eqn}}
By Logarithm is Strictly Increasing:
:$\log \norm y_1^n < \log \norm x_1^m \iff \log \norm y_2^n < \log \norm x_2^m$
By Sum of Logarithms:
:$n \log \norm y_1 < m \log \norm x_1 \iff n \log \norm y_2 < m \log \norm x_2$
Because $m, \log \norm x_1, \log \norm x_2 \ne 0$:
:$r = \dfrac n m < \dfrac {\log \norm x_1} {\log \norm y_1} \iff r = \dfrac n m < \dfrac {\log \norm x_2} {\log \norm y_2}$
By Between two Real Numbers exists Rational Number:
:$\dfrac {\log \norm x_1} {\log \norm y_1} = \dfrac {\log \norm x_2} {\log \norm y_2}$
Because $\log \norm x_2, \log \norm y_2 \ne 0$:
:$\dfrac {\log \norm x_1} {\log \norm x_2} = \dfrac {\log \norm y_1} {\log \norm y_2}$
That is:
:$\alpha = \beta$
{{qed}}
Category:Equivalence of Definitions of Equivalent Division Ring Norms
0w9fh9fzzjpsmeh7kgmw6d8fc585lm2
Theorem: Product with Inverse on Homomorphic Image is Group Homomorphism

Let $G$ be a group.
Let $H$ be an abelian group.
Let $\theta: G \to H$ be a (group) homomorphism.
Let $\phi: G \times G \to H$ be the mapping defined as:
:$\forall \tuple {g_1, g_2} \in G \times G: \map \phi {g_1, g_2} = \map \theta {g_1} \map \theta {g_2}^{-1}$
Then $\phi$ is a homomorphism.

Proof:
First note that from Group Homomorphism Preserves Inverses:
:$\map \theta {g_2}^{-1} = \paren {\map \theta {g_2} }^{-1} = \map \theta { {g_2}^{-1} }$
and so $\map \theta {g_1} \map \theta {g_2}^{-1}$ is not ambiguous:
:$\map \theta {g_1} \map \theta {g_2}^{-1} = \map \theta {g_1} \paren {\map \theta {g_2} }^{-1} = \map \theta {g_1} \map \theta { {g_2}^{-1} }$
From External Direct Product of Groups is Group, $G \times G$ is a group.
Let $a_1, a_2, b_1, b_2 \in G$.
We have:
{{begin-eqn}}
{{eqn | l = \map \phi {a_1 b_1, a_2 b_2}
      | r = \map \theta {a_1 b_1} \map \theta {a_2 b_2}^{-1}
      | c = 
}}
{{eqn | r = \map \theta {a_1 b_1} \paren {\map \theta {a_2 b_2} }^{-1}
      | c = Group Homomorphism Preserves Inverses
}}
{{eqn | r = \map \theta {a_1} \map \theta {b_1} \paren {\map \theta {a_2} \map \theta {b_2} }^{-1}
      | c = {{Defof|Group Homomorphism}}
}}
{{eqn | r = \map \theta {a_1} \map \theta {b_1} \paren {\map \theta {b_2}^{-1} } \paren {\map \theta {a_2}^{-1} }
      | c = Inverse of Group Product
}}
{{eqn | r = \map \theta {a_1} \paren {\map \theta {a_2}^{-1} } \map \theta {b_1} \paren {\map \theta {b_2}^{-1} }
      | c = {{Defof|Abelian Group}}: $H$ is Abelian
}}
{{eqn | r = \map \phi {a_1, a_2} \map \phi {b_1, b_2}
      | c = Definition of $\phi$
}}
{{end-eqn}}
Hence the result by definition of homomorphism.
{{Qed}}
Theorem: Max Operation is Associative

The Max operation is associative:
: $\map \max {\map \max {x, y}, z} = \map \max {x, \max \paren{y, z}}$
Thus we are justified in writing $\map \max {x, y, z}$.

Proof:
To simplify our notation:
: Let $\map \max {x, y}$ be (temporarily) denoted $x \overline \wedge y$
There are the following cases to consider:
:$(1): \quad x \le y \le z$
:$(2): \quad x \le z \le y$
:$(3): \quad y \le x \le z$
:$(4): \quad y \le z \le x$
:$(5): \quad z \le x \le y$
:$(6): \quad z \le y \le x$
Taking each one in turn:
:$(1): \quad$ Let $x \le y \le z$. Then:
{{begin-eqn}}
{{eqn | l = x \overline \wedge \paren{y \overline \wedge z}
      | r = x \overline \wedge z
      | rr= = z
}}
{{eqn | l = \paren{x \overline \wedge y} \overline \wedge z
      | r = y \overline \wedge z
      | rr= = z
}}
{{end-eqn}}
:$(2): \quad$ Let $x \le z \le y$. Then:
{{begin-eqn}}
{{eqn | l = x \overline \wedge \paren{y \overline \wedge z}
      | r = x \overline \wedge y
      | rr= = y
}}
{{eqn | l = \paren{x \overline \wedge y} \overline \wedge z
      | r = y \overline \wedge z
      | rr= = y
}}
{{end-eqn}}
:$(3): \quad$ Let $y \le x \le z$. Then:
{{begin-eqn}}
{{eqn | l = x \overline \wedge \paren{y \overline \wedge z}
      | r = x \overline \wedge z
      | rr= = z
}}
{{eqn | l = \paren{x \overline \wedge y} \overline \wedge z
      | r = x \overline \wedge z
      | rr= = z
}}
{{end-eqn}}
:$(4): \quad$ Let $y \le z \le x$. Then:
{{begin-eqn}}
{{eqn | l = x \overline \wedge \paren{y \overline \wedge z}
      | r = x \overline \wedge z
      | rr= = x
}}
{{eqn | l = \paren{x \overline \wedge y} \overline \wedge z
      | r = x \overline \wedge z
      | rr= = x
}}
{{end-eqn}}
:$(5): \quad$ Let $z \le x \le y$. Then:
{{begin-eqn}}
{{eqn | l = x \overline \wedge \paren{y \overline \wedge z}
      | r = x \overline \wedge y
      | rr= = y
}}
{{eqn | l = \paren{x \overline \wedge y} \overline \wedge z
      | r = y \overline \wedge z
      | rr= = y
}}
{{end-eqn}}
:$(6): \quad$ Let $z \le y \le x$. Then:
{{begin-eqn}}
{{eqn | l = x \overline \wedge \paren{y \overline \wedge z}
      | r = x \overline \wedge y
      | rr= = x
}}
{{eqn | l = \paren{x \overline \wedge y} \overline \wedge z
      | r = x \overline \wedge z
      | rr= = x
}}
{{end-eqn}}
Thus in all cases it can be seen that the result holds.
{{qed}}
Theorem: Min Operation is Associative

The min operation is associative:
:$\map \min {\map \min {x, y}, z} = \map \min {x, \map \min {y, z} }$
Thus we are justified in writing $\map \min {x, y, z}$.

Proof:
To simplify our notation:
:Let $\map \min {x, y}$ be (temporarily) denoted $x \underline \vee y$.
There are the following cases to consider:
:$(1): \quad x \le y \le z$
:$(2): \quad x \le z \le y$
:$(3): \quad y \le x \le z$
:$(4): \quad y \le z \le x$
:$(5): \quad z \le x \le y$
:$(6): \quad z \le y \le x$
Taking each one in turn:
:$(1): \quad$ Let $x \le y \le z$. Then:
{{begin-eqn}}
{{eqn | l = x \underline \vee \paren {y \underline \vee z}
      | r = x \underline \vee y
      | rr= = x
}}
{{eqn | l = \paren {x \underline \vee y} \underline \vee z
      | r = x \underline \vee z
      | rr= = x
}}
{{end-eqn}}
:$(2): \quad$ Let $x \le z \le y$. Then:
{{begin-eqn}}
{{eqn | l = x \underline \vee \paren {y \underline \vee z}
      | r = x \underline \vee z
      | rr= = x
}}
{{eqn | l = \paren {x \underline \vee y} \underline \vee z
      | r = x \underline \vee z
      | rr= = x
}}
{{end-eqn}}
:$(3): \quad$ Let $y \le x \le z$. Then:
{{begin-eqn}}
{{eqn | l = x \underline \vee \paren {y \underline \vee z}
      | r = x \underline \vee y
      | rr= = y
}}
{{eqn | l = \paren {x \underline \vee y} \underline \vee z
      | r = y \underline \vee z
      | rr= = y
}}
{{end-eqn}}
:$(4): \quad$ Let $y \le z \le x$. Then:
{{begin-eqn}}
{{eqn | l = x \underline \vee \paren {y \underline \vee z}
      | r = x \underline \vee y
      | rr= = y
}}
{{eqn | l = \paren {x \underline \vee y} \underline \vee z
      | r = y \underline \vee z
      | rr= = y
}}
{{end-eqn}}
:$(5): \quad$ Let $z \le x \le y$. Then:
{{begin-eqn}}
{{eqn | l = x \underline \vee \paren {y \underline \vee z}
      | r = x \underline \vee z
      | rr= = z
}}
{{eqn | l = \paren {x \underline \vee y} \underline \vee z
      | r = x \underline \vee z
      | rr= = z
}}
{{end-eqn}}
:$(6): \quad$ Let $z \le y \le x$. Then:
{{begin-eqn}}
{{eqn | l = x \underline \vee \paren {y \underline \vee z}
      | r = y \underline \vee z
      | rr= = z
}}
{{eqn | l = \paren {x \underline \vee y} \underline \vee z
      | r = y \underline \vee z
      | rr= = z
}}
{{end-eqn}}
Thus in all cases it can be seen that the result holds.
{{qed}}
Theorem: Theoretical Justification for Cycle Notation

Let $\N_k$ be used to denote the initial segment of natural numbers:
:$\N_k = \closedint 1 k = \set {1, 2, 3, \ldots, k}$
Let $\rho: \N_n \to \N_n$ be a permutation of $n$ letters.
Let $i \in \N_n$.
Let $k$ be the smallest (strictly) positive integer for which $\map {\rho^k} i$ is in the set:
:$\set {i, \map \rho i, \map {\rho^2} i, \ldots, \map {\rho^{k - 1} } i}$
Then:
:$\map {\rho^k} i = i$

Proof:
{{AimForCont}} $\map {\rho^k} i = \map {\rho^r} i$ for some $r > 0$.
As $\rho$ has an inverse in $S_n$:
:$\map {\rho^{k - r} } i = i$
This contradicts the definition of $k$, because $k - r < k$
Thus:
:$r = 0$
The result follows.
{{qed}}
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Norm is Power of Other Norm implies Topologically Equivalent

Let $\norm {\, \cdot \,}_1$ and $\norm {\, \cdot \,}_2$ satisfy:
:$\exists \alpha \in \R_{\gt 0}: \forall x \in R: \norm x_1 = \norm x_2^\alpha$
Then $d_1$ and $d_2$ are topologically equivalent metrics.

Proof:
Let $x \in R$ and $\epsilon \in \R_{\gt 0}$
Then for $y \in R$:
{{begin-eqn}}
{{eqn | l = \norm {y - x}_1 < \epsilon
      | o = \leadstoandfrom
      | r = \norm {y - x}_2^\alpha < \epsilon
}}
{{eqn | o = \leadstoandfrom
      | r = \norm {y - x}_2 < \epsilon^{1 / \alpha}
}}
{{end-eqn}}
Hence:
:$\map {B^1_\epsilon} x = \map {B^2_{\epsilon^{1 / \alpha} } } x$
where:
:$\map {B^1_\epsilon} x$ is the open ball in $d_1$ centered on $x$ with radius $\epsilon$
:$\map {B^2_{\epsilon^{1 / \alpha} } } x$ is the open ball in $d_2$ centered on $x$ with radius $\epsilon^{1 / \alpha}$
Since $x$ and $\epsilon$ were arbitrary then:
:every $d_1$-open ball is a $d_2$-open ball.
Similarly, for $y \in R$:
{{begin-eqn}}
{{eqn | l = \norm {y - x}_2 < \epsilon
      | o = \leadstoandfrom
      | r = \norm {y - x}_2^\alpha < \epsilon^\alpha
}}
{{eqn | o = \leadstoandfrom
      | r = \norm {y - x}_1 < \epsilon^\alpha
}}
{{end-eqn}}
So:
:every $d_2$-open ball is a $d_1$-open ball.
By the definition of an open set of a metric space it follows that $d_1$ and $d_2$ are topologically equivalent metrics,
{{qed}}