avewright/proofwiki-math huggingface dataset:
Theorem: If Compact Between then Way Below

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, k, y \in S$ such that:
:$x \preceq k$ and $k \preceq y$ and $k \in \map K L$
where $\map K L$ denotes the compact subset of $L$.
Then $x \ll y$
where $\ll$ denotes the way below relation.

Proof:
By definition of compact subset:
:$k$ is compact.
By definition of compact:
:$k \ll k$
Thus by Preceding and Way Below implies Way Below:
:$x \ll y$
{{qed}}
Theorem: Nine Regular Polyhedra

There exist $9$ regular polyhedra.

Proof:
From Five Platonic Solids, there exist $5$ regular polyhedra which are convex:
:the regular tetrahedron
:the cube
:the regular octahedron
:the regular dodecahedron
:the regular icosahedron.
From Four Kepler-Poinsot Polyhedra:
{{:Four Kepler-Poinsot Polyhedra}}
All $4$ of the above are regular polyhedra which are non-convex.
making the total $9$.
Theorem: Way Below is Congruent for Join

Let $L = \left({S, \vee, \preceq}\right)$ be a join semilattice.
Then $\ll$ is congruence relation for $\vee$:
:$\forall a, b, x, y \in S: a \ll x \land b \ll y \implies a \vee b \ll x \vee y$
where $\ll$ denotes the way below relation.

Proof:
Let $a, b, x, y \in S$ such that
$a \ll x$ and $b \ll y$
By Join Succeeds Operands:
:$x \preceq x \vee y$ and $y \preceq x \vee y$
By Preceding and Way Below implies Way Below and definition of reflexivity:
:$a \ll x \vee y$ and $b \ll x \vee y$
Thus by Join is Way Below if Operands are Way Below:
:$a \vee b \ll x \vee y$
{{qed}}
Theorem: Lifting The Exponent Lemma

Let $x, y \in \Z$ be distinct integers.
Let $n \ge 1$ be a natural number.
Let $p$ be an odd prime.
Let:
:$p \divides x - y$
and:
:$p \nmid x y$
where $\divides$ and $\nmid$ denote divisibility and non-divisibility respectively.
Then
:$\map {\nu_p} {x^n - y^n} = \map {\nu_p} {x - y} + \map {\nu_p} n$
where $\nu_p$ denotes $p$-adic valuation.

Proof:
=== Lemma ===
{{:Lifting The Exponent Lemma/Lemma}}{{qed|lemma}}
Let $k = \map {\nu_p} n$.
Then $n = p^k m$ such that $p \nmid m$.
By $p$-adic Valuation of Difference of Powers with Coprime Exponent:
:$\map {\nu_p} {x^n - y^n} = \map {\nu_p} {x^{p^k} - y^{p^k} }$
By repeatedly applying the {{Lemma|Lifting The Exponent Lemma}}:
:$\map {\nu_p} {x^{p^k} - y^{p^k} } = \map {\nu_p} {x - y} + k$
{{qed}}
Theorem: Zsigmondy's Theorem

Let $a > b > 0$ be coprime positive integers.
Let $n \ge 1$ be a (strictly) positive integer.
Then there is a prime number $p$ such that
:$p$ divides $a^n - b^n$
:$p$ does not divide $a^k - b^k$ for all $k < n$
with the following exceptions:
:$n = 1$ and $a - b = 1$
:$n = 2$ and $a + b$ is a power of $2$
:$n = 6$, $a = 2$, $b = 1$

Proof:
We call a prime number '''primitive''' if it divides $a^n - b^n$ but not $a^k - b^k$ for any $k < n$.
Let $\map {\Phi_n} {x, y}$ denote the $n$th homogeneous cyclotomic polynomial.
By Product of Cyclotomic Polynomials:
:$a^n - b^n = \ds \prod_{d \mathop \divides n} \map {\Phi_d} {a, b}$
Thus any primitive prime divisor is a divisor of $\map {\Phi_n} {a, b}$.
We start by investigating to which extent the converse is true.
Theorem: Compact Subset is Join Subsemilattice

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\map K L$ be a compact subset of $L$.
Then $\map K L$ is join subsemilattice:
:$\forall x, y \in \map K L: x \vee y \in \map K L$

Proof:
Let $x, y \in \map K L$.
By definition of compact subset:
:$x$ and $y$ are compact.
By definition of compact:
:$x \ll x$ and $y \ll y$
By Way Below is Congruent for Join:
:$x \vee y \ll x \vee y$
By definition:
:$x \vee y$ is compact.
Thus by definition compact subset:
:$x \vee y \in \map K L$
{{qed}}
Theorem: Totally Ordered Ring Zero Precedes Element or its Inverse

Let $\struct {R, +, \circ, \preceq}$ be an ordered ring.
From the definition of ordered ring, $\preceq$ is compatible with $+$.
Let $0_R$ be the zero element of $R$.
Let $x \ne 0_R$ be a non-zero element of $R$.
Let $-x$ be the ring negative of $x$.
Then:
:$0_R \prec x \lor 0_R \prec -x$
but not both.

Proof:
By the definition of total ordering, $\preceq$ is connected.
As $x \ne 0_R$, one of the following is true, but not both:
:$(1): \quad 0_R \prec x$
:$(2): \quad x \prec 0_R$
If $(2)$, because $\prec$ is compatible with $+$:
{{begin-eqn}}
{{eqn | l = x
      | o = \prec 
      | r = 0_R
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-x}
      | o = \prec
      | r = 0_R + \paren {-x}
}}
{{eqn | ll= \leadsto
      | l = 0_R
      | o = \prec
      | r = -x
      | c = {{Defof|Ring Zero}}, {{Defof|Ring Negative}}
}}
{{end-eqn}}
{{qed}}
Category:Ordered Rings
8wp8cg2du1ssfeaen6ry67n4xlytf9l
Theorem: Bottom in Compact Subset

Let $L = \left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.
Then $\bot \in K\left({L}\right)$
where $\bot$ denotes the smallest element of $L$,
:$K\left({L}\right)$ denotes the compact subset of $L$.

Proof:
By Bottom is Way Below Any Element:
:$\bot \ll \bot$
where $\ll$ is the way below relation.
By definition:
:$\bot$ is compact.
Thus by definition of compact subset:
:$\bot \in K\left({L}\right)$
{{qed}}
Theorem: Composition of Relations is not Commutative

Composition of relations is, in general, not commutative.
That is, it is usually the case that:
:$\RR_1 \circ \RR_2 \ne \RR_2 \circ \RR_1$
for relations $\RR_1$ and $\RR_2$.

Proof:
Proof by Counterexample:
Let $\RR_1 := \struct {S, S, R_1}$ and $\RR_2 := \struct {S, S, R_2}$ be relations defined as:
Let:
:$S = \set {0, 1, 2}$
:$R_1 = \set {\tuple {0, 1} }$
:$R_2 = \set {\tuple {1, 2} }$
We have that:
:$\RR_1 \circ \RR_2 = \struct {S, S, \set {\tuple {0, 2} } }$
while:
:$\RR_2 \circ \RR_1 = \struct {S, S, \O}$
{{qed}}
Theorem: Compact Closure is Intersection of Lower Closure and Compact Subset

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $x \in S$.
Then $x^{\mathrm {compact} } = x^\preceq \cap \map K L$
where
:$x^{\mathrm {compact} }$ denotes the compact closure of $x$,
:$x^\preceq$ denotes the lower closure of $x$,
:$\map K L$ denotes the compact subset of $L$.

Proof:
:$y \in x^{\mathrm {compact} }$
{{iff}}
:$y \preceq x$ and $y$ is compact by definition of compact closure
{{iff}}
:$y \in x^\preceq$ and $y$ is compact by definition of lower closure of element
{{iff}}
:$y \in x^\preceq$ and $y \in \map K L$ by definition of compact subset
{{iff}}
:$y \in x^\preceq \cap \map K L$ by definition of intersection
Hence the result, by definition of set equality.
{{qed}}
Theorem: Compact Closure is Subset of Way Below Closure

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $x \in S$.
Then $x^{\mathrm {compact} } \subseteq x^\ll$
where
:$x^{\mathrm {compact} }$ denotes the compact closure of $x$,
:$x^\ll$ denotes the way below closure of $x$.

Proof:
Let $y \in x^{\mathrm {compact} }$.
By definition of compact closure:
:$y \preceq x$ and $y$ is compact.
By definition of compact:
:$y \ll y$
where $\ll$ denotes the way below relation.
By Preceding and Way Below implies Way Below and definition of reflexivity:
:$y \ll x$
Thus by definition of way below closure:
:$y \in x^\ll$
{{qed}}
Theorem: Algebraic iff Continuous and For Every Way Below Exists Compact Between

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a lattice.
Then $L$ is algebraic {{iff}}:
:$L$ is continuous
and:
:$\forall x, y \in S: x \ll y \implies \exists k \in \map K L: x \preceq k \preceq y$
where
:$\ll$ denotes the way below relation,
:$\map K L$ denotes the compact subset of $L$.

Proof:
=== Sufficient Condition ===
Let $L$ be algebraic.
We will prove that
:$\forall x \in S: x^\ll$ is directed
where $x^\ll$ denotes way below closure of $x$.
Let $x \in S$.
By definition of algebraic:
:$x^{\mathrm{compact} }$ is directed
where $x^{\mathrm{compact} }$ denotes the compact closure of $x$.
By Compact Closure is Subset of Way Below Closure:
:$x^{\mathrm{compact} } \subseteq x^\ll$
By definitions of non-empty set and subset:
:$x^\ll \ne \O$
Thus by Non-Empty Way Below Closure is Directed in Join Semilattice:
:$x^\ll$ is directed.
{{qed|lemma}}
Thus by definition of algebraic:
:$L$ is up-complete.
We will prove that:
:$L$ satisfies the axiom of approximation.
Let $x \in S$.
By previous:
:$x^\ll$ is directed.
By definition of algebraic:
:$x^{\mathrm{compact} }$ is directed.
By definition of up-complete:
:$x^\ll$ admits a supremum
and
:$x^{\mathrm{compact} }$ admits a supremum.
By Compact Closure is Subset of Way Below Closure:
:$x^{\mathrm{compact} } \subseteq x^\ll$
By Supremum of Subset:
:$\map \sup {x^{\mathrm {compact} } } \preceq \map \sup {x^\ll}$
By definition of algebraic:
:$L$ satisfies the axiom of $K$-approximation.
By the axiom of $K$-approximation:
:$x \preceq \map \sup {x^\ll}$
By Operand is Upper Bound of Way Below Closure:
:$x$ is an upper bound for $x^\ll$.
By definition of supremum:
:$\map \sup {x^\ll} \preceq x$
Thus by definition of antisymmetry:
:$x = \map \sup {x^\ll}$
{{qed|lemma}}
Hence $L$ is continuous.
Let $x, y \in S$ such that:
:$x \ll y$
By definition of algebraic:
:$D := y^{\mathrm{compact} }$ is directed.
By the axiom of $K$-approximation:
:$y = \sup D$
By definition of way below relation:
:$\exists d \in D: x \preceq d$
By definition of compact closure:
:$d$ is compact.
Thus by definition of compact subset:
:$d \in \map K L$
By definition of supremum:
:$y$ is an upper bound for $D$.
Thus by definition of upper bound:
:$x \preceq d \preceq y$
{{qed|lemma}}
Theorem: Non-Empty Way Below Closure is Directed in Join Semilattice

Let $L = \struct {S, \vee, \preceq}$ be a join semilattice.
Let $x \in S$ such that:
:$x^\ll \ne \O$
where $x^\ll$ denotes the way below closure of $x$.
Then $x^\ll$ is directed.

Proof:
By assumption:
:$x^\ll$ is a non-empty set.
Let $y, z \in x^\ll$.
By definition of way below closure:
:$y \ll x$ and $z \ll x$
By Join is Way Below if Operands are Way Below:
:$y \vee z \ll x$
By definition of way below closure:
:$y \vee z \in x^\ll$
By Join Succeeds Operands:
:$y \preceq y \vee z$ and $z \preceq y \vee z$
Thus by definition:
:$x^\ll$ is directed.
{{qed}}
Theorem: Image under Subset of Relation is Subset of Image under Relation

Let $S$ and $T$ be sets.
Let $\RR_1 \subseteq S \times T$ be a relation in $S \times T$.
Let $\RR_2 \subseteq \RR_1$.
Let $A \subseteq S$.
Then:
:$\RR_2 \sqbrk A \subseteq \RR_1 \sqbrk A$
where $\RR_1 \sqbrk A$ denotes the image of $A$ under $\RR_1$.

Proof:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \RR_2 \sqbrk A
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists x \in A
      | l = \tuple {x, y}
      | o = \in
      | r = \RR_2
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | ll= \leadsto
      | q = \exists x \in A
      | l = \tuple {x, y}
      | o = \in
      | r = \RR_1
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = \RR_1 \sqbrk A
      | c = {{Defof|Image of Subset under Relation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection of Transitive Relations is Transitive/General Result

Let $\family {\RR_i: i \mathop \in I}$ be an $I$-indexed set of transitive relations on a set $S$.
Then their intersection $\ds \bigcap_{i \mathop \in I} \RR_i$ is also a transitive relation on $S$.

Proof:
Let $\ds \tuple {x, y} \in \bigcap_{i \mathop \in I} \RR_i$ and $\ds \tuple {y, z} \in \bigcap_{i \mathop \in I} \RR_i$ be transitive relations on an arbitrary set $S$.
Then by definition of intersection:
:$\tuple {x, y} \in \RR_i$ for all $i \in I$
:$\tuple {y, z} \in \RR_i$ for all $i \in I$
Since each $\RR_i$ is transitive:
:$\tuple {x, z} \in \RR_i$ for all $i \in I$
so, by definition of intersection:
:$\ds \tuple {x, z} \in \bigcap_{i \mathop \in I} \RR_i$
Hence $\ds \bigcap_{i \mathop \in I} \RR_i$ is transitive.
{{qed}}
Category:Intersection of Transitive Relations is Transitive
3dny8dd4lomqcaa7sxpuhg36ppdcbbt
Theorem: Upper Bounds are Equivalent implies Suprema are equal

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $X, Y$ be subsets of $S$.
Assume that
:$X$ admits a supremum
and
:$\forall x \in S: x$ is upper bound for $X \iff x$ is upper bound for $Y$
Then $\sup X = \sup Y$

Proof:
We will prove that
:$\forall b \in S: b$ is upper bound for $Y \implies \sup X \preceq b$
Let $b \in S$ such that
:$b$ is upper bound for $Y$.
By assumption:
:$b$ is upper bound for $X$.
Thus by definition of supremum:
:$\sup X \preceq b$
{{qed|lemma}}
By definition of supremum:
:$\sup X$ is upper bound for $X$.
By assumption:
:$\sup X$ is upper bound for $Y$.
Thus by definition of supremum:
:$\sup X = \sup Y$
{{qed}}
Theorem: Inverse of Subset of Relation is Subset of Inverse

Let $S$ and $T$ be sets
Let $\RR_1 = S \times T$ be a relation on $S \times T$.
Let $\RR_2 \subseteq \RR_1$.
Then:
:$\RR_2^{-1} \subseteq \RR_1^{-1}$
where $\RR_1^{-1}$ denotes the inverse of $\RR_1$.

Proof:
{{begin-eqn}}
{{eqn | l = \tuple {t, s}
      | o = \in
      | r = \RR_2^{-1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {s, t}
      | o = \in
      | r = \RR_2
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {s, t}
      | o = \in
      | r = \RR_1
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {t, s}
      | o = \in
      | r = \RR_1^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{end-eqn}}
The result follows by definition of subset.
{{qed}}
Category:Subsets
Category:Inverse Relations
go17ymoftd92q7gvsjnuspu7i5xiec5
Theorem: Preceding implies if Less Upper Bound then Greater Upper Bound

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $x, y \in S$ such that
:$x \preceq y$
Let $X \subseteq S$.
Then
:$x$ is upper bound for $X \implies y$ is upper bound for $X$
and
:$y$ is lower bound for $X \implies x$ is lower bound for $X$.

Proof:
=== First Implication ===
Let $x$ be upper bound for $X$,
Let $z \in X$.
By definition of upper bound:
:$z \preceq x$
Thus by definition of transitivity:
:$z \preceq y$
{{qed|lemma}}
Theorem: Three Regular Tessellations/Squares

Squares form a regular tessellation:
:400px

Proof:
{{proof wanted}}
Category:Three Regular Tessellations
Category:Squares
nq7qhbj876vmocxcyo6nw999ylgysrj
Theorem: Arithmetic iff Way Below Relation is Multiplicative in Algebraic Lattice

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below algebraic lattice.
Then:
:$L$ is arithmetic
{{iff}}:
:$\ll$ is a multiplicative relation
where $\ll$ denotes the way below relation of $L$.

Proof:
=== Sufficient Condition ===
Let $L$ be arithmetic.
Let $a, x, y \in S$ such that
:$a \ll x$ and $a \ll y$
By Algebraic iff Continuous and For Every Way Below Exists Compact Between:
:$\exists c \in \map K L: a \preceq c \preceq x$
and
:$\exists k \in \map K L: a \preceq k \preceq y$
where $\map K L$ denotes the compact subset of $L$.
By Meet Semilattice is Ordered Structure:
:$c \wedge k \preceq x \wedge y$
By definition of arithmetic:
:$\map K L$ is meet closed.
By definition of meet closed:
:$c \wedge k \in \map K L$
By definition of compact subset:
:$c \wedge k$ is compact.
By definition of compact:
:$c \wedge k \ll c \wedge k$
By Meet is Idempotent:
:$a \wedge a = a$
By Meet Semilattice is Ordered Structure:
:$a \preceq c \wedge k$
Thus by Preceding and Way Below implies Way Below
:$a \ll x \wedge y$
{{qed|lemma}}
Theorem: Endomorphism Ring of Abelian Group is Ring with Unity

Let $\struct {G, +}$ be an abelian group.
Let $\struct {\map {\mathrm {End} } G, \oplus, \circ}$ be its endomorphism ring.
Then $\struct {\map {\mathrm {End} } G, \oplus, \circ}$ is a ring with unity $I_G$, where:
:$I_G$ is the identity mapping on $G$
:$\oplus$ is the pointwise operation on $\map {\mathrm {End} } G$ induced by $+$.

Proof:
{{tidy|throughout, and correction of grammar}}
{{proofread}}
In the below, $f, g , h \in \map {\mathrm {End} } G$.
As $f, g, h$ are (group) endomorphisms, it follows {{afortiori}} that they are also (group) homomorphisms.
Recall that $f \oplus g$ is the pointwise operation on $f$ and $g$ induced by $+$.
We are given that $\struct {G, +}$ is an abelian group.
Hence $\struct {G, +}$ is {{afortiori}} a commutative semigroup.
By Homomorphism on Induced Structure to Commutative Semigroup, $f \oplus g$ is a homomorphism from $\struct {G, +}$ into $\struct {G, +}$.
So, by definition, $f \oplus g$ is an endomorphism on $\struct {G, +}$.
{{improve|Better to prove that $\struct {\map {\mathrm {End} } G, \oplus}$ is a group, then invoke {{Ring-axiom|A|nolink}}.}}
Now, taking the ring axioms in turn:
Theorem: Elements of Finite Support form Submagma of Direct Product

Let $\struct {S_i, \circ_i}_{i \mathop \in I}$ be a family of magmas with identity.
Let $\ds S = \prod_{i \mathop \in I} S_i$ be their direct product.
Let $T$ be the subset of elements of $S$ whose support is finite:
:$T = \set {s \in S: \map \supp s \text{ is finite} }$
Then $T$ is a submagma of $S$.

Proof:
From Finite Subsets form Ideal, the set of finite subsets of $I$ form an ideal of $I$.
From Elements with Support in Ideal form Submagma of Direct Product, $T$ is a submagma of $S$.
Category:Direct Products
0ktxy08bwzt1vfvd8mca0qi51wrsjov
Theorem: Möbius Inversion Formula/Abelian Group

Let $G$ be an abelian group.
Let $f, g: \N \to G$ be mappings.
Then
:$\ds \map f n = \prod_{d \mathop \divides n} \map g d$
{{iff}}:
:$\ds \map g n = \prod_{d \mathop \divides n} \map f d^{\mu \paren {\frac n d} }$

Proof:
{{ProofWanted|The proof should go in the same way as in the main theorem ($G {{=}} \R$ or $\C$).}}
Category:Möbius Inversion Formula
Category:Abelian Groups
Category:Möbius Function
okdav3r3k2kigfwpo1mhiw4bpdiovx7
Theorem: Möbius Inversion Formula for Cyclotomic Polynomials

Let $n > 0$ be a (strictly) positive integer.
Let $\Phi_n$ be the $n$th cyclotomic polynomial.
Then:
:$\map {\Phi_n} x = \ds \prod_{d \mathop \divides n} \paren {x^d - 1}^{\map \mu {n / d} }$
where:
:the product runs over all divisors of $n$
:$\mu$ is the Möbius function.

Proof:
By Product of Cyclotomic Polynomials:
:$\ds \prod_{d \mathop \divides n} \map {\Phi_d} x = x^n - 1$
for all $n \in \N$.
The nonzero rational forms form an abelian group under multiplication.
By the Möbius inversion formula for abelian groups, this implies:
:$\ds \map {\Phi_n} x = \prod_{d \mathop \divides n} \paren {x^d - 1}^{\map \mu {n / d} }$
for all $n \in \N$.
{{qed}}
Category:Cyclotomic Polynomials
myti7upv7fpx4y2yct66mkz9608l8ud
Theorem: Composite of Inverse of Mapping with Mapping

Let $f: S \to T$ be a mapping.
Then:
:$f \circ f^{-1} = I_{\Img f}$
where:
: $f \circ f^{-1}$ is the composite of $f$ and $f^{-1}$
: $f^{-1}$ is the inverse of $f$
: $I_{\Img f}$ is the identity mapping on the image set of $f$.

Proof:
By Inverse of Mapping is One-to-Many Relation, $f^{-1}$ is a one-to-many relation:
:$f^{-1} \subseteq T \times S$
whose domain is the image set of $f$.
By definition of composition of relations:
:$f \circ f^{-1} := \set {\tuple {x, z} \in T \times T: \exists y \in S: \tuple {x, y} \in f^{-1} \land \tuple {y, z} \in f}$
Thus $f \circ f^{-1}$ is a relation on $T \times T$.
Let $x \in \Img f$.
Then:
:$\exists y \in S: \tuple {x, y} \in f^{-1}$
As $f$ is a mapping, and so by definition a many-to-one relation;
:$\map f y = x$
for all $y$ such that $\tuple {x, y} \in f^{-1}$.
That is:
:$\forall x \in \Img f: f \circ \map {f^{-1} } x = x$
Hence the result by definition of identity mapping.
{{qed}}
Theorem: Equivalence of Definitions of Order Complete Set

Let $\struct {S, \preceq}$ be an ordered set.
{{TFAE|def = Order Complete Set}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $\struct {S, \preceq}$ be an order complete set by definition 1.
Let $H \subseteq S$ have a lower bound.
Let $K$ be the set of all lower bounds of $H$.
Then $K \ne \O$.
By definition of lower bound:
:$\forall x \in K: \forall y \in H: x \le y$
and so all elements of $H$ are upper bounds of $K$.
Thus by hypothesis $K$ admits a supremum.
Let $k = \map \sup K$.
By definition of supremum, $k$ precedes every upper bound of $K$.
In particular, $k$ precedes every element of $H$.
Thus $k$ is a lower bound of $H$.
But we have that $k$ is an upper bound of $K$.
That is, $k$ succeeds every lower bound of $H$.
That is, $k$ is an infimum of $H$.
Thus $\struct {S, \preceq}$ is an order complete set by definition 2.
{{qed|lemma}}
Theorem: Condition for Uniqueness of Increasing Mappings between Tosets

Let $\struct {S, \preceq}$ and $\struct {T, \preccurlyeq}$ be tosets.
Let $f: S \to T$ and $g: S \to T$ be increasing mappings from $S$ to $T$.
Let $H \subseteq S$ be a subset of $S$.
Let $f$ and $g$ agree on $H$.
Let $K = f \sqbrk H$ be the image set of $H$ under $f$.
Let the intersection of $K$ with every set of the form:
:$\set {y \in T: u < y < v: u, v \in T, u < v}$
be non-empty.
Then $f = g$.

Proof:
By hypothesis, let the intersection of $K$ with every set of the form:
:$\set {y \in T: u \prec y \prec v: u, v \in T, u \prec v}$
be non-empty.
{{AimForCont}} $f \ne g$.
Then:
:$\exists x \in S: \map f x \ne \map g x$
{{WLOG}}, suppose that $\map f x < \map g x$.
Let:
:$a \in H$ such that $a \preceq x$
:$b \in H$ such that $b \succeq x$
We have that $f$ and $g$ are increasing.
Thus:
:$\map f a \preccurlyeq \map f x$
:$\map g b \succcurlyeq \map g x$
Thus no element of $H$ maps to the set:
:$\set {y \in T: \map f x \prec y \prec \map g x}$
That is, the intersection of $K$ with this set, which is of the form:
:$\set {y \in T: u \prec y \prec v: u, v \in T, u \prec v}$
is empty.
This contradicts our hypothesis.
Thus, by Proof by Contradiction:
:$f = g$
{{qed}}
Theorem: Characteristic of Increasing Mapping from Toset to Order Complete Toset

Let $\struct {S, \preceq}$ and $\struct {T, \preccurlyeq}$ be tosets.
Let $T$ be order complete.
Let $H \subseteq S$ be a subset of $S$.
Let $f: H \to T$ be an increasing mapping from $H$ to $T$.
Then:
:$f$ has an extension to $S$ which is increasing
{{iff}}:
:for all $A \subseteq H$: if $A$ is bounded in $S$, then $f \sqbrk A$ is bounded in $T$
where $f \sqbrk A$ denotes the image set of $A$ under $f$.

Proof:
=== Necessary Condition ===
Suppose $f$ is such that it is not the case that:
:for all $A \subseteq H$: if $A$ is bounded in $S$, then $f \sqbrk A$ is bounded in $T$.
Proof by Counterexample:
Let $S = \R_{>0}$ be the set of all (strictly) positive real numbers.
Let $H \subseteq S$ be the open real interval $H = \openint 0 1$.
Let $T = H$.
By the axiomatic definition of real numbers, $S$ and $T$ are totally ordered.
From the Continuum Property, $T$ is order complete.
Let $f: H \to T$ be the identity mapping.
Note that while $H$ has an upper bound in $S$, for example $1$
Let $y \in T$ be an upper bound of $f \sqbrk H$.
By construction:
:$y < 1$
and so:
:$\exists \epsilon \in \R_{>0}: y + \epsilon = 1$
Thus:
:$y < y + \dfrac \epsilon 2 < 1$
and so there exists $y' = y + \dfrac \epsilon 2 \in T$ such that:
:$y < y'$
and such that:
:$y' = \map f {y'} \in f \sqbrk H$
So $y$ is not an upper bound of $f \sqbrk H$.
Thus $f \sqbrk H$ has no upper bound in $T$.
Let $g: S \to T$ be an extension of $f$ to $S$.
Consider $\map g 1$.
We have that $1$ is an upper bound of $H$.
Let $\map g 1 = y$.
As $y \in \openint 0 1$ it follows that:
:$y > 1$
and so:
:$\exists \epsilon \in \R_{>0}: y + \epsilon = 1$
But then:
:$y < y + \dfrac \epsilon 2 < 1$
and so:
:$\map g 1 < \map g {y + \dfrac \epsilon 2}$
and so $g$ is not increasing.
Thus it has been demonstrated that if it is not the case that:
:for all $A \subseteq H$: if $A$ is bounded in $S$, then $f \sqbrk A$ is bounded in $T$
where:
:$\struct {S, \preceq}$ and $\struct {T, \preccurlyeq}$ be tosets
and:
:$T$ is order complete
and:
:$f: H \to T$ is an increasing mapping from $H$ to $T$.
and:
:$H \subseteq S$ is a subset of $S$
then it is not necessarily the case that $f$ always has an extension to $S$ which is increasing.
{{qed|lemma}}