avewright/proofwiki-math huggingface dataset:
Theorem: Normal to Curve is Tangent to Evolute

Let $C$ be a curve defined by a real function which is twice differentiable.
Let the curvature of $C$ be non-constant.
Let $P$ be a point on $C$.
Let $Q$ be the center of curvature of $C$ at $P$.
The normal to $C$ at $P$ is tangent to the evolute $E$ of $C$ at $Q$.

Proof:
:400px
Let $P = \tuple {x, y}$ be a general point on $C$.
Let $Q = \tuple {X, Y}$ be the center of curvature of $C$ at $P$.
From the above diagram:
:$(1): \quad \begin{cases} x - X = \pm \rho \sin \psi \\ Y - y = \pm \rho \cos \psi \end{cases}$
where:
:$\rho$ is the radius of curvature of $C$ at $P$
:$\psi$ is the angle between the tangent to $C$ at $P$ and the $x$-axis.
Whether the sign is plus or minus depends on whether the curve is convex or concave.
For simplicity, let it be assumed that the curvature $k$ at each point under consideration on $C$ is positive.
The case for $k < 0$ can then be treated similarly.
Thus we have $k > 0$ and so $(1)$ can be written:
:$(2): \quad \begin{cases} X = x - \rho \sin \psi \\ Y = y +\rho \cos \psi \end{cases}$
By definition of curvature:
:$k = \dfrac {\d \psi} {\d s}$
and:
:$\rho = \dfrac 1 k = \dfrac {\d s} {\d \psi}$
Hence:
{{begin-eqn}}
{{eqn | l = \rho \sin \psi
      | r = \dfrac {\d s} {\d \psi} \dfrac {\d y} {\d s}
      | c = 
}}
{{eqn | n = 3
      | r = \dfrac {\d y} {\d \psi}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \rho \cos \psi
      | r = \dfrac {\d s} {\d \psi} \dfrac {\d x} {\d s}
      | c = 
}}
{{eqn | n = 4
      | r = \dfrac {\d x} {\d \psi}
      | c = 
}}
{{end-eqn}}
Differentiating $(2)$ {{WRT|Differentiation}} $\psi$:
{{begin-eqn}}
{{eqn | l = \dfrac {\d X} {\d \psi}
      | r = \dfrac {\d x} {\d \psi} - \rho \cos \psi - \dfrac {\d \rho} {\d \psi} \sin \psi
      | c = 
}}
{{eqn | r = - \dfrac {\d \rho} {\d \psi} \sin \psi
      | c = from $(3)$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \dfrac {\d Y} {\d \psi}
      | r = \dfrac {\d y} {\d \psi} - \rho \sin \psi + \dfrac {\d \rho} {\d \psi} \cos \psi
      | c = 
}}
{{eqn | r = \dfrac {\d \rho} {\d \psi} \cos \psi
      | c = from $(4)$
}}
{{end-eqn}}
By assumption, $\dfrac {\d \rho} {\d \psi} \ne 0$ on $C$.
Hence we have:
{{begin-eqn}}
{{eqn | l = \dfrac {\d Y} {\d X}
      | r = -\dfrac {\cos \psi} {\sin \psi}
      | c = 
}}
{{eqn | r = -\dfrac 1 {\tan \psi}
      | c = 
}}
{{end-eqn}}
We have Slope of Normal is Minus Reciprocal of Tangent.
Thus the slope of the tangent to $E$ equals the slope of the normal to $C$.
The result follows.
Note the case when $\dfrac {\d \rho} {\d \psi} = 0$ on $C$.
In this case $C$ is a circle.
By Evolute of Circle is its Center its evolute is a single point and so has no tangent.
{{qed}}
Theorem: Length of Arc of Evolute equals Difference in Radii of Curvature

Let $C$ be a curve defined by a real function which is twice differentiable.
Let the curvature of $C$ be non-constant.
The length of arc of the evolute $E$ of $C$ between any two points $Q_1$ and $Q_2$ of $C$ is equal to the difference between the radii of curvature at the corresponding points $P_1$ and $P_2$ of $C$.

Proof:
:400px
Let $P = \tuple {x, y}$ be a general point on $C$.
Let $Q = \tuple {X, Y}$ be the center of curvature of $C$ at $P$.
From the above diagram:
:$(1): \quad \begin {cases} x - X = \pm \rho \sin \psi \\ Y - y = \pm \rho \cos \psi \end {cases}$
where:
:$\rho$ is the radius of curvature of $C$ at $P$
:$\psi$ is the angle between the tangent to $C$ at $P$ and the $x$-axis.
Whether the sign is plus or minus depends on whether the curve is convex or concave.
For simplicity, let it be assumed that the curvature $k$ at each point under consideration on $C$ is positive.
The case for $k < 0$ can then be treated similarly.
Thus we have $k > 0$ and so $(1)$ can be written:
:$(2): \quad \begin {cases} X = x - \rho \sin \psi \\ Y = y +\rho \cos \psi \end {cases}$
By definition of curvature:
:$k = \dfrac {\d \psi} {\d s}$
and:
:$\rho = \dfrac 1 k = \dfrac {\d s} {\d \psi}$
Hence:
{{begin-eqn}}
{{eqn | l = \rho \sin \psi
      | r = \dfrac {\d s} {\d \psi} \dfrac {\d y} {\d s}
      | c = 
}}
{{eqn | n = 3
      | r = \dfrac {\d y} {\d \psi}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \rho \cos \psi
      | r = \dfrac {\d s} {\d \psi} \dfrac {\d x} {\d s}
      | c = 
}}
{{eqn | n = 4
      | r = \dfrac {\d x} {\d \psi}
      | c = 
}}
{{end-eqn}}
Differentiating $(2)$ {{WRT|Differentiation}} $\psi$:
{{begin-eqn}}
{{eqn | l = \dfrac {\d X} {\d \psi}
      | r = \dfrac {\d x} {\d \psi} - \rho \cos \psi - \dfrac {\d \rho} {\d \psi} \sin \psi
      | c = 
}}
{{eqn | n = 5
      | r = - \dfrac {\d \rho} {\d \psi} \sin \psi
      | c = from $(3)$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \dfrac {\d Y} {\d \psi}
      | r = \dfrac {\d y} {\d \psi} - \rho \sin \psi + \dfrac {\d \rho} {\d \psi} \cos \psi
      | c = 
}}
{{eqn | n = 6
      | r = \dfrac {\d \rho} {\d \psi} \cos \psi
      | c = from $(4)$
}}
{{end-eqn}}
Let $S$ be the length of arc of the evolute $E$ from a fixed point $Q_0$ on $E$ to the variable point $Q$ corresponding to $P$.
We have that:
:$\d S^2 = \d X^2 + \d Y^2$
and so:
{{begin-eqn}}
{{eqn | l = \paren {\dfrac {\d S} {\d \psi} }^2
      | r = \paren {\dfrac {\d X} {\d \psi} }^2 + \paren {\dfrac {\d Y} {\d \psi} }^2
      | c = 
}}
{{eqn | r = \paren {- \dfrac {\d \rho} {\d \psi} \sin \psi}^2 + \paren {\dfrac {\d \rho} {\d \psi} \cos \psi}^2
      | c = from $(5)$ and $(6)$
}}
{{eqn | r = \paren {\dfrac {\d \rho} {\d \psi} }^2 \paren {\sin^2 \psi + \cos^2 \psi}
      | c = 
}}
{{eqn | r = \paren {\dfrac {\d \rho} {\d \psi} }^2 
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Choosing the direction of $S$ so that $S$ and $\rho$ increase together, this tells us:
:$\dfrac {\d S} {\d \psi} = \dfrac {\d \rho} {\d \psi}$
Integrating {{WRT|Integration}} $\psi$ gives:
:$S = \rho + c$
where $c$ is a constant.
{{qed}}
Theorem: Curve is Involute of Evolute

Let $C$ be a curve defined by a real function which is twice differentiable.
Let the curvature of $C$ be non-constant.
Let $E$ be the evolute $C$.
Then the involute of $E$ is $C$.

Proof:
From Length of Arc of Evolute equals Difference in Radii of Curvature:
:the length of arc of the evolute $E$ of $C$ between any two points $Q_1$ and $Q_2$ of $C$ is equal to the difference between the radii of curvature at the corresponding points $P_1$ and $P_2$ of $C$.
Thus $C$ exhibits precisely the property of the involute of $E$.
{{qed}}
Theorem: Evolute of Cycloid is Cycloid

The evolute of a cycloid is another cycloid.

Proof:
Let $C$ be the cycloid defined by the equations:
:$\begin {cases} x = a \paren {\theta - \sin \theta} \\ y = a \paren {1 - \cos \theta} \end {cases}$
From Parametric Equations for Evolute: Formulation 2:
:$(1): \quad \begin {cases} X = x - \dfrac {y' \paren {x'^2 + y'^2} } {x' y' ' - y' x' '} \\ Y = y + \dfrac {x' \paren {x'^2 + y'^2} } {x' y' ' - y' x' '} \end {cases}$
where:
:$\tuple {x, y}$ denotes the Cartesian coordinates of a general point on $C$
:$\tuple {X, Y}$ denotes the Cartesian coordinates of a general point on the evolute of $C$
:$x'$ and $x' '$ denote the derivative and second derivative respectively of $x$ {{WRT|Differentiation}} $\theta$
:$y'$ and $y' '$ denote the derivative and second derivative respectively of $y$ {{WRT|Differentiation}} $\theta$.
Thus we have:
{{begin-eqn}}
{{eqn | l = x'
      | r = a \paren {1 - \cos \theta}
      | c = 
}}
{{eqn | l = x' '
      | r = a \sin \theta
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = y'
      | r = a \sin \theta
      | c = 
}}
{{eqn | l = y' '
      | r = a \cos \theta
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac {x'^2 + y'^2} {x' y' ' - y' x' '}
      | r = \dfrac {a^2 \paren {1 - \cos \theta}^2 + a^2 \sin^2 \theta} {a \paren {1 - \cos \theta} a \cos \theta - a \sin \theta \, a \sin \theta}
      | c = substituting for $x'$, $x' '$, $y'$, $y' '$
}}
{{eqn | r = \dfrac {\paren {1 - 2 \cos \theta + \cos^2 \theta} + \sin^2 \theta} {\cos \theta - \cos^2 \theta - \sin^2 \theta}
      | c = multiplying out, cancelling out $a^2$
}}
{{eqn | r = \dfrac {2 - 2 \cos \theta} {\cos \theta - 1}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | n = 2
      | r = -2
      | c = dividing top and bottom by $1 - \cos \theta$
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = X
      | r = a \paren {\theta - \sin \theta} - a \sin \theta \paren {-2}
      | c = substituting for $x$ and $y'$ and from $(2)$ in $(1)$
}}
{{eqn | r = a \paren {\theta + \sin \theta}
      | c = simplifying
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = Y
      | r = a \paren {1 - \cos \theta} + a \paren {1 - \cos \theta} \paren {-2}
      | c = substituting for $y$ and $x'$ and from $(2)$ in $(1)$
}}
{{eqn | r = -a \paren {1 - \cos \theta}
      | c = 
}}
{{end-eqn}}
The cycloid $C$ (blue) and its evolute (red) are illustrated below:
600px
{{qed}}
Theorem: Meet of Directed Subsets is Directed

Let $\struct {S, \preceq}$ be a meet semilattice.
Let $D_1, D_2$ be directed subset of $S$.
Then:
:$\set {x \wedge y: x \in D_1, y \in D_2}$ is a directed subset of $S$.

Proof:
Let $a, b \in \set {x \wedge y: x \in D_1, y \in D_2}$.
Then:
:$\exists x \in D_1, y \in D_2: a = x \wedge y$
and
:$\exists z \in D_1, t \in D_2: b = z \wedge t$
By definition of directed subset:
:$\exists g \in D_1: x \preceq g \land z \preceq g$
and
:$\exists h \in D_2: y \preceq h \land t \preceq h$
By Meet Semilattice is Ordered Structure:
:$x \wedge y \preceq g \wedge h$ and $z \wedge t \preceq g \wedge h$
:$g \wedge h \in \set {x \wedge y: x \in D_1, y \in D_2}$
Thus:
:$\exists c \in \set {x \wedge y: x \in D_1, y \in D_2}: a \preceq c \land b \preceq c$
Hence by definition:
:$\set {x \wedge y: x \in D_1, y \in D_2}$ is directed.
{{qed}}
Theorem: Image of Directed Subset under Increasing Mapping is Directed

Let $\left({S, \preceq}\right)$, $\left({T, \precsim}\right)$ be ordered sets.
Let $f: S \to T$ be an increasing mapping.
Let $D$ be a directed subset of $S$.
Then
:$f^\to \left({D}\right)$ is also a directed subset of $T$
where
:$f^\to \left({D}\right)$ denotes the image of $D$ under $f$.

Proof:
Let $x, y \in f^\to\left({D}\right)$.
By definition of image of set:
:$\exists a \in D: x = f \left({a}\right)$
and
:$\exists b \in D: y = f \left({b}\right)$
By definition of directed subset:
:$\exists c \in D: a \preceq c \land b \preceq c$
By definition of image of set:
:$f\left({c}\right) \in f^\to\left({D}\right)$
By definition of increasing mapping:
:$x \precsim f\left({c}\right)$ and $y \precsim f\left({c}\right)$
Thus by definition
:$f^\to\left({D}\right)$ is a directed subset of $T$.
{{qed}}
Theorem: Mass of Sun from Universal Gravitational Constant

Let the universal gravitational constant be known.
Let the mean distance from the Earth to the sun be known.
Then it is possible to calculate the mass of the sun.

Proof:
From Kepler's Third Law of Planetary Motion:
:$T^2 = \paren {\dfrac {4 \pi^2} {G M} } a^3$
where:
:$T$ is the orbital period of the planet in question (in this case, the Earth)
:$a$ is the distance from the planet (in this case, the Earth) to the sun
:$M$ is the mass of the sun
:$G$ is the universal gravitational constant
In MKS units:
:$T = 60 \times 60 \times 24 \times 365.24219 \, \mathrm s$ by definition of year
:$a = 149 \, 597 \, 870 \, 700 \, \mathrm m$ by definition of astronomical unit
:$G = 6.674 \times 10^{-11} \, \mathrm N \, \mathrm m^2 \, \mathrm{kg}^{-2}$ by measurement, as {{hypothesis}}.
:$M$ will be the result in kilograms.
Thus:
{{begin-eqn}}
{{eqn | l = M
      | r = \dfrac {4 \pi^2 a^3} {T^2 G}
      | c = 
}}
{{eqn | r = \frac {4 \times \paren {3.14159}^2 \times \paren {149.60 \times 10^9}^3} {\paren {31.557 \times 10^6} \times 6.674 \times 10^{-11} }
      | c = 
}}
{{end-eqn}}
The calculation has been left as an exercise for anyone who has the patience.
{{qed}}
Theorem: Meet is Directed Suprema Preserving implies Meet of Suprema equals Supremum of Meet of Directed Subsets

Let $\struct {S, \preceq}$ be an up-complete meet semilattice.
Let $\struct {S \times S, \precsim}$ be the simple order product of $\struct {S, \preceq}$ and $\struct {S, \preceq}$.
Let $f: S \times S \to S$ be a mapping such that:
:$\forall s, t \in S: \map f {s, t} = s \wedge t$
and:
:$f$ preserves directed suprema.
Let $D_1, D_2$ be directed subsets of $S$.
Then:
:$\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {x \wedge y: x \in D_1, y \in D_2}$

Proof:
By Up-Complete Product:
:$\struct {S \times S, \precsim}$ is up-complete.
By Up-Complete Product/Lemma 1:
:$D_1 \times D_2$ is directed subsets of $S \times S$
By definition of mapping preserves directed suprema:
:$f$ preserves the supremum of $D_1 \times D_2$
By definition of up-complete:
:$D_1 \times D_2$ admits a supremum
and:
$D_1$ and $D_2$ admit suprema.
Thus:
{{begin-eqn}}
{{eqn | l = \paren {\sup D_1} \wedge \paren {\sup D_2}
      | r = \map f {\sup D_1, \sup D_2}
      | c = Definition of $f$
}}
{{eqn | r = \map f {\map \sup {D_1 \times D_2} }
      | c = Supremum of Simple Order Product
}}
{{eqn | r = \map \sup {\map {f^\to} {D_1 \times D_2} }
      | c = Mapping Preserves Supremum
}}
{{eqn | r = \sup \set {\map f {x, y}: \tuple {x, y} \in D_1 \times D_2}
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | r = \sup \set {x \wedge y: x \in D_1, y \in D_2}
      | c = Definition of $f$
}}
{{end-eqn}}
{{qed}}
Theorem: Meet of Suprema equals Supremum of Meet of Ideals implies Ideal Supremum is Meet Preserving

Let $\mathscr S = \struct {S, \wedge, \preceq}$ be an up-complete meet semilattice.
Let $f: \map {\it Ids} {\mathscr S} \to S$ be a mapping such that:
:$\forall I \in \map {\it Ids} {\mathscr S}: \map f I = \sup_{\mathscr S} I$
where 
:$\map {\it Ids} {\mathscr S}$ denotes the set of all ideals in $\mathscr S$
Let
:$\forall I_1, I_2 \in \map {\it Ids} {\mathscr S}: \paren {\sup I_1} \wedge \paren {\sup I_2} = \sup \set {i \wedge j: i \in I_1, j \in I_2}$
Then:
$f$ preserves meet as a mapping from $\struct {\map {\it Ids} {\mathscr S}, \subseteq}$ into $\mathscr S$

Proof:
Let $I, J \in \map {\it Ids} {\mathscr S}$ such that
:$\set {I, J}$ admits an infimum in $\struct {\map {\it Ids} {\mathscr S}, \subseteq}$.
By definition of image of set:
:$\map {f^\to} {\set {I, J} } = \set {\map f I, \map f J}$
Thus by definition of meet semilattice:
:$\map {f^\to} {\set {I, J} }$ admits an infimum in $\mathscr S$.
Thus:
{{begin-eqn}}
{{eqn | l = \map \inf {\map {f^\to} {\set {I, J} } }
      | r = \map f I \wedge \map f J
      | c = {{Defof|Meet (Order Theory)}}
}}
{{eqn | r = \paren {\sup I} \wedge \paren {\sup J}
      | c = Definition of $f$
}}
{{eqn | r = \sup \set {x \wedge y: x \in I, y \in J}
      | c = Assumption
}}
{{eqn | r = \map \sup {I \wedge J}
      | c = Meet in Set of Ideals
}}
{{eqn | r = \map f {I \wedge J}
      | c = definition of $f$
}}
{{eqn | r = \map f {\inf \set {I, J} }
      | c = {{Defof|Meet (Order Theory)}}
}}
{{end-eqn}}
{{qed}}
Theorem: Quaternion Multplication is not Commutative

The operation of multplication on the quaternions $H$ is not commutative.

Proof:
By definition of multplication:
{{begin-eqn}}
{{eqn | l = \mathbf i \times \mathbf j
      | r = \mathbf k
      | c = 
}}
{{eqn | l = \mathbf j \times \mathbf i
      | r = -\mathbf k
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Field Norm of Quaternion is not Norm

Let $\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$ be a quaternion.
Let $\overline {\mathbf x}$ be the conjugate of $\mathbf x$.
The field norm of $\mathbf x$:
:$\map n {\mathbf x} := \size {\mathbf x \overline {\mathbf x} }$
is not a norm in the abstract algebraic context of a division ring.

Proof:
Each of the norm axioms is examined in turn:
Theorem: Field Norm of Quaternion is Positive Definite

Let $\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$ be a quaternion.
Let $\overline {\mathbf x}$ be the conjugate of $\mathbf x$.
The field norm of $\mathbf x$:
:$\map n {\mathbf x} := \cmod {\mathbf x \overline {\mathbf x} }$
is positive definite.

Proof:
{{begin-eqn}}
{{eqn | l = \map n {\mathbf x}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \cmod {\mathbf x \overline {\mathbf x} }
      | r = 0
      | c = {{Defof|Field Norm of Quaternion}}
}}
{{eqn | ll= \leadstoandfrom
      | l = a^2 + b^2 + c^2 + d^2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a = 0, b = 0, c = 0, d = 0
      | o = 
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k
      | r = \mathbf 0
      | c = 
}}
{{end-eqn}}
Hence $n$ is positive definite by definition.
{{qed}}
Theorem: Field Norm of Quaternion is Multiplicative

Let $\mathbf x$ be a quaternion.
Let $\overline {\mathbf x}$ be the conjugate of $\mathbf x$.
The field norm of $\mathbf x$:
:$\map n {\mathbf x} := \size {\mathbf x \overline {\mathbf x} }$
is a multiplicative function.

Proof:
{{begin-eqn}}
{{eqn | l = \map n {\mathbf x \mathbf y}
      | r = \mathbf x \, \mathbf y \ \overline {\mathbf x \, \mathbf y}
      | c = {{Defof|Field Norm of Quaternion}}
}}
{{eqn | r = \mathbf x \, \mathbf y \paren {\overline {\mathbf y} \, \overline {\mathbf x} }
      | c = Product of Quaternion Conjugates
}}
{{eqn | r = \mathbf x \paren {\mathbf y \paren {\overline {\mathbf y} \, \overline {\mathbf x} } }
      | c = 
}}
{{eqn | r = \mathbf x \paren {\paren {\mathbf y \, \overline {\mathbf y} } \overline {\mathbf x} }
      | c = 
}}
{{eqn | r = \mathbf x \paren {\map n {\mathbf y} \overline {\mathbf x} }
      | c = 
}}
{{eqn | r = \map n {\mathbf y} \paren {\mathbf x \, \overline {\mathbf x} }
      | c = 
}}
{{eqn | r = \map n {\mathbf y} \, \map n {\mathbf x}
      | c = 
}}
{{eqn | r = \map n {\mathbf x} \, \map n {\mathbf y}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Oscillation of Real Function at Point

Let $X$ and $Y$ be real sets.
Let $f: X \to Y$ be a real function.
Let $x \in X$.
{{TFAE|def = Oscillation of Real Function at Point}}

Proof:
=== Definitions 1 and 2 are equivalent ===
We reformulate Definition 1 into Definition 1' by:
:substituting the definition of $\map {\omega_f} {U \cap X}$ into the definition of $\map {\omega_f} x$
Definition 1':
:$\ds \map {\omega_f} x := \inf_{U \mathop \in \NN_x} \paren {\sup_{y, z \mathop \in U \cap X} \size {\map f y - \map f z} }$
We reformulate Definition 2 into Definition 2' by:
:substituting the definition of $\map {\omega_f} {\openint {x - \epsilon} {x + \epsilon} \cap X}$ into the definition of $\map {\omega_f} x$
:changing set condition into sup tag
Definition 2':
:$\ds \map {\omega_f} x := \inf_{\epsilon \mathop \in \R_{>0} } \paren {\sup_{y, z \mathop \in \openint {x - \epsilon} {x + \epsilon} \cap X} \size {\map f y - \map f z} }$
The theorem text of Oscillation at Point (Infimum) equals Oscillation at Point (Epsilon-Neighborhood) also contains two definitions of Oscillation at a Point for a real function $f$.
We call them definitions $a)$ and $b)$.
Definition $a)$:
Let $\NN_x$ be the set of neighborhoods of $x$.
:$\map {\omega_f} x = \ds \inf \set {\map {\omega_f} {I \cap X}: I \in \NN_x}$
where:
:$\map {\omega_f} {I \cap X} = \ds \sup \set {\size {\map f y - \map f z}: y, z \in I \cap X}$
Definition $b)$:
:$\map {\omega^E_f} x = \inf \set {\map {\omega_f} {I \cap X}: I \in E_x}$
where:
:$E_x$ is the set of $\epsilon$-neighborhoods of $x$
We reformulate Definition $a)$ into Definition $a')$ by:
:substituting the definition of $\map {\omega_f} {I \cap X}$ into the definition of $\map {\omega_f} x$
:changing set conditions into sup tags
:renaming parameter set $I$ to $U$
Definition $a')$:
:$\ds \map {\omega_f} x = \inf_{U \mathop \in \NN_x} \paren {\sup_{y, z \mathop \in U \cap X} \size {\map f y - \map f z} }$
We reformulate Definition $b)$ into Definition $b')$ by:
:substituting the definition of $\map {\omega_f} {I \cap X}$ into the definition of $\map {\omega^E_f} x$
:changing set conditions into sup tags
:using $\epsilon$ as parameter instead of $I$
Definition $b')$:
:$\ds \map {\omega^E_f} x = \inf_{\epsilon \mathop \in \R_{>0}} \paren {\sup_{y, z \mathop \in \openint {x - \epsilon} {x + \epsilon} \cap X} \size {\map f y - \map f z} }$
We observe that definitions $(1')$ and $a')$ are the same, so they are equivalent.
Therefore:
:Definition 1 and $a)$ are equivalent
Also, definitions $(2')$ and $b')$ are the same, so they are equivalent.
Therefore:
:Definition 2 and $b)$ are equivalent
We have:
:Definition 1 and Definition $a)$ are equivalent
:Definition $a)$ and Definition $b)$ are equivalent by Oscillation at Point (Infimum) equals Oscillation at Point (Epsilon-Neighborhood)
:Definition $b)$ and Definition 2 are equivalent
Therefore:
:Definition 1 and Definition 2 are equivalent
{{qed|lemma}}
Theorem: Complex Numbers cannot be Extended to Algebra in Three Dimensions with Real Scalars

It is not possible to extend the complex numbers to an algebra of $3$ dimensions with real scalars.

Proof:
{{AimForCont}} that $\set {1, i, j}$ forms a basis for an algebra of $3$ dimensions with real scalars.
Let $1$ and $i$ have their usual properties as they do as complex numbers:
:$\forall a: 1 a = a 1 = a$
:$i \cdot i = -1$
Then:
:$i j = a_1 + a_2 i + a_3 j$
for some $a_1, a_2, a_3 \in \R$.
Multiplying through by $i$:
:$(1): \quad i \paren {i j} = \paren {i i} j = -j$
and:
{{begin-eqn}}
{{eqn | l = i \paren {a_1 + a_2 i + a_3 j}
      | r = a_1 i - a_2 + a_3 i j
      | c = 
}}
{{eqn | r = a_1 i - a_2 + a_3 \paren {a_1 + a_2 i + a_3 j}
      | c = 
}}
{{eqn | r = a_1 i - a_2 + a_1 a_3 + a_2 a_3 i + {a_3}^2 j
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = \paren {a_1 a_3 - a_2} + \paren {a_1 + a_2 a_3} i + \paren { {a_3}^2 + 1} j
      | c = from $(1)$
}}
{{end-eqn}}
But this implies that ${a_3}^2 = -1$, which contradicts our supposition that $a_3 \in \R$.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Supremum of Simple Order Product

Let $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$ be ordered sets.
Let $\struct {S_1 \times S_2, \precsim}$ be the simple order product of $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$.
Let $X_1$ be a non-empty subset of $S_1$, $X_2$ be a non-empty subset of $S_2$ such that
:$X_1$ and $X_2$ admit suprema.
Then:
:$X_1 \times X_2$ admits a supremum
and:
:$\map \sup {X_1 \times X_2} = \tuple {\sup X_1, \sup X_2}$

Proof:
We will prove that:
:$\tuple {\sup X_1, \sup X_2}$ is upper bound for $X_1 \times X_2$
Let $\tuple {a, b} \in X_1 \times X_2$.
By definition of Cartesian product:
:$a \in X_1$ and $b \in X_2$
By definitions of supremum and upper bound:
:$a \preceq_1 \sup X_1$ and $b \preceq_2 \sup X_2$
Thus by definition of simple order product:
:$\tuple {a, b} \precsim \tuple {\sup X_1, \sup X_2}$
{{qed|lemma}}
We will prove that:
:$\forall \tuple {a, b} \in S1 \times S_2: \tuple {a, b}$ is upper bound for $X_1 \times X_2 \implies \tuple {\sup X_1, \sup X_2} \precsim \tuple {a, b}$
Let $\tuple {a, b} \in S1 \times S_2$ such that:
:$\tuple {a, b}$ is upper bound for $X_1 \times X_2$
We will prove as sublemma that:
:$a$ is upper bound for $X_1$
Let $c \in X_1$.
By definition of non-empty set:
:$\exists d: d \in X_2$
By definition of Cartesian product:
:$\tuple {c, d} \in X_1 \times X_2$
By definition of upper bound:
:$\tuple {c, d} \precsim \tuple {a, b}$
Thus by definition of simple order product:
:$c \preceq_1 a$
This ends the proof of sublemma.
Analogically we have that:
:$b$ is upper bound for $X_2$
By definition of supremum:
:$\sup X_1 \preceq_1 a$ and $\sup X_2 \preceq_2 b$
Thus by definition of simple order product:
:$\tuple {\sup X_1, \sup X_2} \precsim \tuple {a, b}$
{{qed|lemma}}
Thus by definition:
:$X_1 \times X_2$ admits a supremum
and:
:$\map \sup {X_1 \times X_2} = \tuple {\sup X_1, \sup X_2}$
{{qed}}
Theorem: Vectors in Three Dimensional Space with Cross Product forms Lie Algebra

Let $S$ be the set of vectors in $3$ dimensional Euclidean space.
Let $\times$ denote the vector cross product on $S$.
Then $\struct {S, \times}$ is a Lie algebra.

Proof:
By definition of Lie algebra, it suffices to prove two properties:
:$(1): \forall a \in S: a \times a = 0$
:$(2): \forall a, b, c \in S: a \times \paren {b \times c} + b \times \paren {c \times a} + c \times \paren {a \times b} = 0$