avewright/proofwiki-math huggingface dataset:
Theorem: Integral of Positive Simple Function is Positive Homogeneous

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \R, f \in \EE^+$ be a positive simple function.
Let $\lambda \in \R_{\ge 0}$ be a positive real number.
Then:
:$\map {I_\mu} {\lambda \cdot f} = \map {\lambda \cdot I_\mu} f$
where:
:$\lambda \cdot f$ is the pointwise $\lambda$-multiple of $f$
:$I_\mu$ denotes $\mu$-integration.
This can be summarized by saying that $I_\mu$ is positive homogeneous.

Proof:
Remark that $\lambda \cdot f$ is a positive simple function by Scalar Multiple of Simple Function is Simple Function.
Let:
:$f = \ds \sum_{i \mathop = 0}^n a_i \chi_{E_i}$
be a standard representation for $f$.
Then we also have, for all $x \in X$:
{{begin-eqn}}
{{eqn | l = \map {\lambda \cdot f} x
      | r = \lambda \sum_{i \mathop = 0}^n a_i \map {\chi_{E_i} } x
}}
{{eqn | r = \sum_{i \mathop = 0}^n \paren {\lambda a_i} \map {\chi_{E_i} } x
      | c = Summation is Linear
}}
{{end-eqn}}
and it is immediate from the definition that this yields a standard representation for $\lambda \cdot f$.
Therefore, we have:
{{begin-eqn}}
{{eqn | l = \map {\lambda \cdot I_\mu} f
      | r = \lambda \sum_{i \mathop = 0}^n a_i \map \mu {E_i}
      | c = {{Defof|Integral of Positive Simple Function|$\mu$-Integration}}
}}
{{eqn | r = \sum_{i \mathop = 0}^n \paren {\lambda a_i} \map \mu {E_i}
      | c = Summation is Linear
}}
{{eqn | r = \map {I_\mu} {\lambda \cdot f}
      | c = {{Defof|Integral of Positive Simple Function|$\mu$-Integration}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Strict Ordering Preserved under Product with Invertible Element

Let $\struct {S, \circ, \preceq}$ be an ordered semigroup.
Let $z \in S$ be invertible.
Suppose that either $x \circ z \prec y \circ z$ or $z \circ x \prec z \circ y$.
Then $x \prec y$.

Proof:
Suppose $x \circ z \prec y \circ z$.
By Invertible Element of Monoid is Cancellable, $z^{-1}$ is cancellable.
Then from Strict Ordering Preserved under Product with Cancellable Element:
:$x = \paren {x \circ z} \circ z^{-1} \prec \paren {y \circ z} \circ z^{-1} = y$
Likewise, if $z \circ x \prec z \circ y$:
:$x = z^{-1} \circ \paren {z \circ x} \prec z^{-1} \circ \paren {z \circ y} = y$
{{qed}}
Theorem: Strict Ordering Preserved under Cancellability in Totally Ordered Semigroup

Let $\struct {S, \circ, \preceq}$ be a totally ordered semigroup.
If either:
:$x \circ z \prec y \circ z$
or
:$z \circ x \prec z \circ y$
then $x \prec y$.

Proof:
Let $x \circ z \prec y \circ z$.
{{AimForCont}} $x \succeq y$.
As $\struct {S, \circ, \preceq}$ is an ordered semigroup, $\preceq$ is compatible with $\circ$.
Hence we have:
:$x \succeq y \implies x \circ z \succeq y \circ z$
which contradicts $x \circ z \prec y \circ z$.
We have that $\preceq$ is a total ordering, and that it is not the case that $x \succeq y$.
Hence by the Trichotomy Law:
:$x \prec y$
Similarly for $z \circ x \prec z \circ y$.
{{qed}}
Theorem: Relation Compatibility in Totally Ordered Semigroup

Let $\left({S, \circ, \preceq}\right)$ be an ordered semigroup such that:
:$(1): \quad$ All the elements of $\left({S, \circ, \preceq}\right)$ are cancellable for $\circ$
:$(2): \quad \preceq$ is a total ordering.
Then:
:$\forall x, y, z \in S: x \circ z \preceq y \circ z \iff x \preceq y$

Proof:
From Strict Ordering Preserved under Cancellability in Totally Ordered Semigroup:
: $x \circ z \prec y \circ z \implies x \prec y$
From the definition of cancellable element:
: $x \circ z = y \circ z \implies x = y$
{{qed}}
Category:Ordered Semigroups
oafce8s0w7tw3us87tqoozua1fopu57
Theorem: Integral of Positive Measurable Function Extends Integral of Positive Simple Function

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \R, f \in \EE^+$ be a positive simple function.
Then:
:$\ds \int f \rd \mu = \map {I_\mu} f$
where:
:$\ds \int \cdot \rd \mu$ denotes the $\mu$-integral of positive measurable functions
:$I_\mu$ denotes the $\mu$-integral of positive simple functions.
That is:
:$\ds \int \cdot \rd \mu \restriction_{\EE^+} = I_\mu$
using the notion of restriction, $\restriction$.

Proof:
From the definition of the integral of a positive measure function, we have: 
:$\ds \int f \rd \mu = \sup \set {\map {I_\mu} g: g \le f, g \in \EE^+}$
Let $g \in \EE^+$ be such that $g \le f$. 
Then, from Integral of Positive Simple Function is Increasing, we have: 
:$\map {I_\mu} g \le \map {I_\mu} f$ 
So $\map {I_\mu} f$ is an upper bound of $\set {\map {I_\mu} g: g \le f, g \in \EE^+}$. 
Since $f \in \EE^+$, and $f \le f$, we have: 
:$\map {I_\mu} f \in \set {\map {I_\mu} g: g \le f, g \in \EE^+}$
So:
:$\map {I_\mu} f$ is the greatest element of $\set {\map {I_\mu} g: g \le f, g \in \EE^+}$.
so, from Greatest Element is Supremum:
:$\map {I_\mu} f = \sup \set {\map {I_\mu} g: g \le f, g \in \EE^+}$
So:
:$\ds \int f \rd \mu = \map {I_\mu} f$
{{qed}}
Theorem: Ordered Semigroup Isomorphism is Surjective Monomorphism

Let $\struct {S, \circ, \preceq}$ and $\struct {T, *, \preccurlyeq}$ be ordered semigroups.
Let $\phi: \struct {S, \circ, \preceq} \to \struct {T, *, \preccurlyeq}$ be a mapping.
Then $\phi$ is an ordered semigroup isomorphism {{iff}}:
:$(1): \quad \phi$ is an ordered semigroup monomorphism
:$(2): \quad \phi$ is a surjection.

Proof:
=== Necessary Condition ===
Let $\phi: \struct {S, \circ, \preceq} \to \struct {T, *, \preccurlyeq}$ be an ordered semigroup isomorphism.
Then by definition:
:$\phi$ is a semigroup isomorphism from the semigroup $\struct {S, \circ}$ to the semigroup $\struct {T, *}$
:$\phi$ is an order isomorphism from the ordered set $\struct {S, \preceq}$ to the ordered set $\struct {T, \preccurlyeq}$.
A semigroup isomorphism is by definition:
:A semigroup homomorphism
which is:
:A monomorphism and an epimorphism.
From Order Isomorphism is Surjective Order Embedding, an order isomorphism is an order embedding which is also a surjection.
Putting this all together, we see that an ordered semigroup isomorphism is:
:A monomorphism
:An order embedding
:A surjection.
An ordered semigroup monomorphism is by definition: 
:A monomorphism
which is also
:An order embedding
Hence $\phi$ is:
:An ordered semigroup monomorphism
:A surjection.
{{qed|lemma}}
Theorem: Ordered Semigroup Monomorphism into Image is Isomorphism

Let $\struct {S, \circ, \preceq}$ and $\struct {T, *, \preccurlyeq}$ be ordered semigroups.
Let $\phi: \struct {S, \circ, \preceq} \to \struct {T, *, \preccurlyeq}$ be an ordered semigroup monomorphism.
Let $S'$ be the image of $\phi$.
Then $\phi$ is an ordered semigroup isomorphism from $\struct {S, \circ, \preceq}$ into $\struct {S', * {\restriction_{S'} }, \preccurlyeq \restriction_{S'} }$.
Here:
:$* {\restriction_{S'}}$ denotes the restriction of $*$ to $S' \times S'$
:$\preccurlyeq \restriction_{S'}$ denotes the restriction of $\preccurlyeq$ to $S' \times S'$.

Proof:
Let $\phi: \struct {S, \circ, \preceq} \to \struct {T, *, \preccurlyeq}$ be an ordered semigroup monomorphism.
Then $\phi$ is an injection into $\struct {T, *, \preccurlyeq}$ by definition.
From Restriction of Mapping to Image is Surjection, a mapping from a set to the image of that mapping is a surjection.
Thus the surjective restriction of $\phi$ onto $S'$ is an ordered semigroup monomorphism which is also a surjection.
Hence the result from Ordered Semigroup Isomorphism is Surjective Monomorphism.
{{qed}}
Theorem: Order Completion is Unique up to Isomorphism

Let $\struct {S, \preceq_S}$ be an ordered set.
Suppose that both $\struct {T, \preceq_T}$ and $\struct {T', \preceq_{T'} }$ are order completions for $\struct {S, \preceq_S}$.
Then there exists a unique order isomorphism $\psi: T \to T'$.
In particular, $\struct {T, \preceq_T}$ and $\struct {T', \preceq_{T'} }$ are isomorphic.

Proof:
Both $\struct {T, \preceq_T}$ and $\struct {T', \preceq_{T'} }$ are order completions for $\struct {S, \preceq_S}$.
Hence they both satisfy condition $(4)$ (and also $(1)$, $(2)$ and $(3)$).
Thus, applying condition $(4)$ to $\struct {T, \preceq_T}$ (with respect to $\struct {T', \preceq_{T'} }$), obtain a unique increasing mapping $\phi: T' \to T$.
Applying $(4)$ to $\struct {T', \preceq_{T'} }$ (with respect to $\struct {T, \preceq_T}$) gives also a unique increasing mapping $\psi: T \to T'$.
By Composite of Increasing Mappings is Increasing, their composites $\psi \circ \phi: T' \to T'$ and $\phi \circ \psi: T \to T$ are also increasing.
Now applying $(4)$ to $\struct {T, \preceq_T}$ (with respect to itself), it follows that $\phi \circ \psi$ is unique.
Now from Identity Mapping is Order Isomorphism, the identity mapping $I_T: T \to T$ is also increasing.
Thus, uniqueness of $\phi \circ \psi$ implies that $\phi \circ \psi = I_T$.
Similarly, it follows that $\psi \circ \phi = I_{T'}$.
It follows that $\psi: T \to T'$ is a bijection from Bijection iff Left and Right Inverse.
Thus, $\psi$ is an order-preserving bijection whose inverse is also increasing.
That is, $\psi$ is an order isomorphism.
Its uniqueness was already remarked above.
{{qed}}
Category:Order Theory
ngzuyc67phbhtocx2lv0cm6z3gnrms2
Theorem: Intersection of Strict Upper Closures in Toset

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $a, b \in S$.
Then:
:$a^\succ \cap b^\succ = \paren {\map \max {a, b} }^\succ$
where:
:$a^\succ$ denotes strict upper closure of $a$
:$\max$ denotes the max operation.

Proof:
As $\struct {S, \preceq}$ is a totally ordered set, have either $a \preceq b$ or $b \preceq a$.
Both sides are seen to be invariant upon interchanging $a$ and $b$.
{{WLOG}}, then, let $a \preceq b$.
Then it follows by definition of $\max$ that:
:$\map \max {a, b} = b$
Thus, from Intersection with Subset is Subset, it suffices to show that $b^\succ \subseteq a^\succ$.
By definition of strict upper closure, this comes down to showing that:
:$\forall c \in S: b \prec c \implies a \prec c$
So let $c \in S$ with $b \prec c$, and recall that $a \preceq b$.
By Strictly Precedes is Strict Ordering, $a \prec c$.
{{qed}}
Theorem: Intersection of Weak Upper Closures in Toset

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $a, b \in S$.
Then:
:$a^\succcurlyeq \cap b^\succcurlyeq = \paren {\map \max {a, b} }^\succcurlyeq$
where:
:$a^\succcurlyeq$ denotes weak upper closure of $a$
:$\max$ denotes the max operation.

Proof:
As $\struct {S, \preccurlyeq}$ is a totally ordered set, either $a \preccurlyeq b$ or $b \preccurlyeq a$.
Both sides are seen to be invariant upon interchanging $a$ and $b$.
{{WLOG}}, let $a \preccurlyeq b$.
Then it follows by definition of $\max$ that:
:$\map \max {a, b} = b$
Thus, from Intersection with Subset is Subset, it suffices to show that:
:$b^\succcurlyeq \subseteq a^\succcurlyeq$
By definition of weak upper closure, this comes down to showing that:
:$\forall c \in S: b \preccurlyeq c \implies a \preccurlyeq c$
So let $c \in S$ with $b \preccurlyeq c$.
Recall that $a \preccurlyeq b$.
Now as $\preccurlyeq$ is a total ordering, it is in particular transitive.
Hence $a \preccurlyeq c$.
{{qed}}
Theorem: Intersection of Weak Lower Closures in Toset

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $a, b \in S$.
Then:
:$a^\preccurlyeq \cap b^\preccurlyeq = \paren {\min \set {a, b} }^\preccurlyeq$
where:
:$a^\preccurlyeq$ denotes the weak lower closure of $a$
:$\min$ denotes the min operation.

Proof:
As $\struct {S, \preccurlyeq}$ is a totally ordered set, either $a \preccurlyeq b$ or $b \preccurlyeq a$.
Both sides are seen to be invariant upon interchanging $a$ and $b$.
{{WLOG}}, let $b \preccurlyeq a$.
Then it follows by definition of $\min$ that $\min \set {a, b} = b$.
Thus, from Intersection with Subset is Subset, it suffices to show that:
:$b^\preccurlyeq \subseteq a^\preccurlyeq$
By definition of weak lower closure, this comes down to showing that:
:$\forall c \in S: c \preccurlyeq b \implies c \preccurlyeq a$
So let $c \in S$ with $c \preccurlyeq b$.
Recall that $b \preccurlyeq a$.
Now as $\preccurlyeq$ is a total ordering, it is in particular transitive.
Hence $c \preccurlyeq a$.
{{qed}}
Theorem: Intersection of Strict Lower Closures in Toset

Let $\left({S, \preceq}\right)$ be a totally ordered set.
Let $a,b \in S$.
Then:
:$a^\prec \cap b^\prec = \left({\min \left({a, b}\right)}\right)^\prec$
where:
: $a^\prec$ denotes strict lower closure of $a$
: $\min$ denotes the min operation.

Proof:
As $\left({S, \preceq}\right)$ is a totally ordered set, have either $a \preceq b$ or $b \preceq a$.
Since both sides are seen to be invariant upon interchanging $a$ and $b$, let WLOG $b \preceq a$.
Then it follows by definition of $\min$ that $\min \left({a, b}\right) = b$.
Thus, from Intersection with Subset is Subset, it suffices to show that $b^\prec \subseteq a^\prec$.
By the definition of strict lower closure, this comes down to showing that:
:$\forall c \in S: c \prec b \implies c \prec a$
So let $c \in S$ with $c \prec b$, and recall that $b \preceq a$.
By Strictly Precedes is Strict Ordering, $c \prec a$.
{{qed}}
Theorem: Naturally Ordered Semigroup Exists

Let the Zermelo-Fraenkel axioms be accepted as axiomatic.
Then there exists a '''naturally ordered semigroup'''.

Proof:
We take as axiomatic the Zermelo-Fraenkel axioms.
From these, Minimally Inductive Set Exists is demonstrated.
This proves the existence of a minimally inductive set.
Then we have that the Minimally Inductive Set forms Peano Structure.
It follows that the existence of a Peano structure depends upon the existence of such a minimally inductive set.
Then we have that a Naturally Ordered Semigroup forms Peano Structure.
Hence the result.
{{qed}}
Theorem: Strict Upper Closure in Restricted Ordering

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$ be a subset of $S$, and let $\preceq \restriction_T$ be the restricted ordering on $T$.
Then for all $t \in T$:
:$t^{\succ T} = T \cap t^{\succ S}$
where:
:$t^{\succ T}$ is the strict upper closure of $t$ in $\struct {T, \preceq \restriction_T}$
:$t^{\succ S}$ is the strict upper closure of $t$ in $\struct {S, \preceq}$.

Proof:
Let $t \in T$, and suppose that $t' \in t^{\succ T}$.
By definition of strict upper closure, this is equivalent to:
:$t \preceq \restriction_T t' \land t \ne t'$
By definition of $\preceq \restriction_T$, the first condition comes down to:
:$t \preceq t' \land t' \in T$
as it is assumed that $t \in T$.
In conclusion, $t' \in t^{\succ T}$ is equivalent to:
:$t' \in T \land t \preceq t' \land t \ne t'$
These last two conjuncts precisely express that $t' \in t^{\succ S}$.
By definition of set intersection, it also holds that:
:$t' \in T \cap t^{\succ S}$
{{iff}} $t' \in T$ and $t' \in t^{\succ S}$.
Thus, it follows that the following are equivalent:
:$t' \in t^{\succ T}$
:$t' \in T \cap t^{\succ S}$
and hence the result follows, by definition of set equality.
{{qed}}
Category:Upper Closures
efck8d5y20zacp5g8adhq48haepksvq
Theorem: Weak Upper Closure in Restricted Ordering

Let $\struct {S, \preccurlyeq}$ be an ordered set.
Let $T \subseteq S$ be a subset of $S$.
Let $\preccurlyeq \restriction_T$ be the restricted ordering on $T$.
Then for all $t \in T$:
:$t^{\succcurlyeq T} = T \cap t^{\succcurlyeq S}$
where:
:$t^{\succcurlyeq T}$ is the weak upper closure of $t$ in $\struct {T, \preccurlyeq \restriction_T}$
:$t^{\succcurlyeq S}$ is the weak upper closure of $t$ in $\struct {S, \preccurlyeq}$.

Proof:
Let $t \in T$.
Suppose that:
:$t' \in t^{\succcurlyeq T}$
By definition of weak upper closure $t^{\succcurlyeq T}$, this is equivalent to:
:$t \preccurlyeq \restriction_T t'$
By definition of $\preccurlyeq \restriction_T$, this comes down to:
:$t \preccurlyeq t' \land t' \in T$
as it is assumed that $t \in T$.
The first conjunct precisely expresses that $t' \in t^{\succcurlyeq S}$.
By definition of set intersection, it also holds that:
:$t' \in T \cap t^{\succcurlyeq S}$
{{iff}} $t' \in T$ and $t' \in t^{\succcurlyeq S}$.
Thus it follows that the following are equivalent:
:$t' \in t^{\succcurlyeq T}$
:$t' \in T \cap t^{\succcurlyeq S}$
and hence the result follows, by definition of set equality.
{{qed}}
Category:Upper Closures
1qwalv9cuiv4cwdokeredjk1iemd5sh
Theorem: Strict Lower Closure in Restricted Ordering

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $T \subseteq S$ be a subset of $S$, and let $\preceq \restriction_T$ be the restricted ordering on $T$.
Then for all $t \in T$:
:$t^{\prec T} = T \cap t^{\prec S}$
where:
: $t^{\prec T}$ is the strict lower closure of $t$ in $\left({T, \preceq \restriction_T}\right)$
: $t^{\prec S}$ is the strict lower closure of $t$ in $\left({S, \preceq}\right)$.

Proof:
Let $t \in T$, and suppose that $t' \in t^{\prec T}$.
By definition of strict lower closure, this is equivalent to:
:$t' \preceq \restriction_T t \land t \ne t'$
By definition of $\preceq \restriction_T$, the first condition comes down to:
:$t' \preceq t \land t' \in T$
as it is assumed that $t \in T$.
In conclusion, $t' \in t^{\prec T}$ is equivalent to:
:$t' \in T \land t' \preceq t \land t \ne t'$
These last two conjuncts precisely express that $t' \in t^{\prec S}$.
By definition of set intersection, it also holds that:
:$t' \in T \cap t^{\prec S}$
{{iff}} $t' \in T$ and $t' \in t^{\prec S}$.
Thus, it follows that the following are equivalent:
:$t' \in t^{\prec T}$
:$t' \in T \cap t^{\prec S}$
and hence the result follows, by definition of set equality.
{{qed}}
Category:Lower Closures
6myrp2u4ncp6ly3ixesdftk3jnumgk2
Theorem: Weak Lower Closure in Restricted Ordering

Let $\left({S, \preccurlyeq}\right)$ be an ordered set.
Let $T \subseteq S$ be a subset of $S$.
Let $\preccurlyeq \restriction_T$ be the restricted ordering on $T$.
Then for all $t \in T$:
:$t^{\preccurlyeq T} = T \cap t^{\preccurlyeq S}$
where:
:$t^{\preccurlyeq T}$ is the weak lower closure of $t$ in $\left({T, \preccurlyeq \restriction_T}\right)$
:$t^{\preccurlyeq S}$ is the weak lower closure of $t$ in $\left({S, \preccurlyeq}\right)$.

Proof:
Let $t \in T$, and suppose that $t' \in t^{\preccurlyeq T}$.
By definition of weak lower closure $t^{\preccurlyeq T}$, this is equivalent to:
:$t' \preccurlyeq \restriction_T t$
By definition of $\preccurlyeq \restriction_T$, this comes down to:
:$t' \preccurlyeq t \land t' \in T$
as it is assumed that $t \in T$.
The first conjunct precisely expresses that $t' \in t^{\preccurlyeq S}$.
By definition of set intersection, it also holds that:
:$t' \in T \cap t^{\preccurlyeq S}$
{{iff}} $t' \in T$ and $t' \in t^{\preccurlyeq S}$.
Thus, it follows that the following are equivalent:
:$t' \in t^{\preccurlyeq T}$
:$t' \in T \cap t^{\preccurlyeq S}$
and hence the result follows, by definition of set equality.
{{qed}}
Category:Lower Closures
ec7t0bq4r2xcy1qwf2wnubvomk7ykta
Theorem: Order Topology on Natural Numbers is Discrete Topology

Let $\le$ be the standard ordering on the natural numbers $\N$.
Then the order topology $\tau$ on $\N$ is the discrete topology.

Proof:
By Topology is Discrete iff All Singletons are Open, it suffices to show that for all $n \in \N$, the singleton $\set n$ is an open of $\tau$.
Now observe that $\map \downarrow 1 = \set 0$, since for all $n \in \N$, $n < 1 \implies n = 0$.
It follows that $\set 0$ is an open set of $\tau$.
Suppose now that $n \in \N$ and $n \ne 0$.
Then it is known that for all $m \in \N$, $n - 1 < m < n + 1$ implies $m = n$.
Thus, $\map {\mathop{\uparrow} } {n - 1} \cap \map {\mathop{\downarrow} } {n + 1} = \set n$.
It follows that $\set n$ is an open set of $\tau$.
{{explain|arrows, and why this inference holds (using the def'n of order top as gen. top)}}
Hence the result, from Proof by Cases.
{{qed}}
Category:Order Topologies
Category:Discrete Topologies
Category:Natural Numbers
g6it316r6ps1zagw83g5h9pzic9o6eh
Theorem: Natural Numbers under Multiplication form Ordered Commutative Semigroup

Let $\N$ be the natural numbers.
Let $\times$ be multiplication.
Let $\le$ be the ordering on $\N$.
Then $\struct {\N, \times, \le}$ is an ordered commutative semigroup.

Proof:
By Natural Numbers under Multiplication form Semigroup, $\struct {\N, \times, \le}$ is a semigroup.
By Natural Number Multiplication is Commutative, $\times$ is commutative.
By Ordering on Natural Numbers is Compatible with Multiplication, $\le$ is compatible with $\times$.
The result follows.
{{qed}}
Theorem: Invertible Elements under Natural Number Multiplication

Let $\N$ be the natural numbers.
Let $\times$ denote multiplication.
Then the only invertible element of $\N$ for $\times$ is $1$.

Proof:
$m \in \N$ is invertible for $\times$.
Let $n \in \N: m \times n = 1$.
Then from Natural Numbers have No Proper Zero Divisors:
:$m \ne 0$ and $n \ne 0$
Thus, $1 \le m$ and $1 \le n$.
If $1 \le m$ then from Ordering on Natural Numbers is Compatible with Multiplication:
:$1 \le n < m \times n$
This contradicts $m \times n = 1$.
The result follows.
{{qed}}
Theorem: Graph containing Closed Walk of Odd Length also contains Odd Cycle

Let $G$ be a graph.
{{explain|This proof works for a simple graph, but the theorem may hold for loop graphs and/or multigraphs. Clarification needed as to what applies.}}
Let $G$ have a closed walk of odd length.
Then $G$ has an odd cycle.

Proof:
Let $G = \struct {V, E}$ be a graph with closed walk whose length is odd.
From Closed Walk of Odd Length contains Odd Circuit, such a walk contains a circuit whose length is odd.
Let $C_1 = \tuple {v_1, \ldots, v_{2 n + 1} = v_1}$ be such a circuit.
{{AimForCont}} $G$ has no odd cycles.
Then $C_1$ is not a cycle.
Hence, there exist a vertex $v_i$ where $2 \le i \le 2 n - 1$ and an integer $k$ such that $i + 1 \le k \le 2 n$ and $v_i = v_k$.
If $k - i$ is odd, then we have an odd circuit $\tuple {v_i, \ldots, v_k = v_i}$ smaller in length than $C_1$.
If $k - i$ is even, then $\tuple {v_1, \ldots, v_i, v_{k + 1}, \ldots, v_{2 n + 1} }$ is a circuit whose length is odd smaller in length than $C_2$.
This new odd length circuit is named $C_2$, and the same argument is applied as to $C_1$.
Thus at each step a circuit whose length is odd is reduced.
At the $n$th step for some $n \in \N$, either:
:$(1): \quad C_n$ is a cycle, which contradiction the supposition that $G$ has no odd cycles
or:
:$(2): \quad C_n$ is a circuit whose length is $3$.
But from Circuit of Length 3 is Cycle, $C_n$ is a cycle, which by definition has odd length.
From this contradiction it follows that $G$ has at least one odd cycle.
{{qed}}
Category:Graph Theory
l8zk3p3w030bszq9nvlwr04h5kd69ds
Theorem: Homomorphism of Powers/Naturally Ordered Semigroup

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
For a given $a \in T_1$, let $\map {\odot^n} a$ be the $n$th power of $a$ in $T_1$.
For a given $a \in T_2$, let $\map {\oplus^n} a$ be the $n$th power of $a$ in $T_2$.
Then:
:$\forall a \in T_1: \forall n \in \struct {S^*, \circ, \preceq}: \map \phi {\map {\odot^n} a} = \map {\oplus^n} {\map \phi a}$
where $S^* = S \setminus \set 0$.

Proof:
The proof proceeds by the Principle of Mathematical Induction for a Naturally Ordered Semigroup.
Let $A := \set {n \in S^*: \forall a \in T_1: \map \phi {\map {\odot^n} a} = \map {\oplus^n} {\map \phi a} }$
That is, $A$ is defined as the set of all $n$ such that:
:$\forall a \in T_1 \map \phi {\map {\odot^n} a} = \map {\oplus^n} {\map \phi a}$
Theorem: Homomorphism of Powers/Natural Numbers

Let $n \in \N$.
Let $\odot^n$ and $\oplus^n$ be the $n$th powers of $\odot$ and $\oplus$, respectively.
Then:
:$\forall a \in T_1: \forall n \in \N: \map \phi {\map {\odot^n} a} = \map {\oplus^n} {\map \phi a}$

Proof:
Consider the natural numbers $\N$ defined as a naturally ordered semigroup.
Then the result follows from Homomorphism of Powers: Naturally Ordered Semigroup.
{{qed}}
Category:Homomorphism of Powers
Category:Natural Numbers
lxnxcsdzoy5a8ayu5kvqqyojyw99bn8