avewright/proofwiki-math huggingface dataset:
Theorem: Power Set with Union and Subset Relation is Ordered Semigroup

Let $S$ be a set and let $\powerset S$ be its power set.
Let $\struct {\powerset S, \cup, \subseteq}$ be the ordered structure formed from the set union operation and subset relation.
Then $\struct {\powerset S, \cup, \subseteq}$ is an ordered semigroup.

Proof:
From Power Set with Union is Commutative Monoid, $\struct {\powerset S, \cup}$ is {{afortiori}} a semigroup.
From Subset Relation is Ordering, $\struct {\powerset S, \subseteq}$ is an ordered set.
It remains to be shown that $\subseteq$ is compatible with $\cup$.
Let $A, B \subseteq S$ be arbitrary such that $A \subseteq B$.
Thus:
{{begin-eqn}}
{{eqn | l = A
      | o = \subseteq
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall T \subseteq S
      | l = A \cup T
      | o = \subseteq
      | r = B \cup T
      | c = Set Union Preserves Subsets: Corollary
}}
{{eqn | ll= \leadsto
      | q = \forall T \subseteq S
      | l = T \cup A
      | o = \subseteq
      | r = T \cup B
      | c = Union is Commutative
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Power Set with Union and Superset Relation is Ordered Semigroup

Let $S$ be a set and let $\powerset S$ be its power set.
Let $\struct {\powerset S, \cup, \supseteq}$ be the ordered structure formed from the set union operation and superset relation.
Then $\struct {\powerset S, \cup, \supseteq}$ is an ordered semigroup.

Proof:
From Power Set with Union is Commutative Monoid, $\struct {\powerset S, \cup}$ is {{afortiori}} a semigroup.
From Subset Relation is Ordering, $\struct {\powerset S, \subseteq}$ is an ordered set.
We have that $\supseteq$ is the dual to $\subseteq$.
Hence $\struct {\powerset S, \supseteq}$ is an ordered set.
It remains to be shown that $\supseteq$ is compatible with $\cup$.
Let $A, B \subseteq S$ be arbitrary such that $A \supseteq B$.
Thus:
{{begin-eqn}}
{{eqn | l = A
      | o = \supseteq
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall T \subseteq S
      | l = A \cup T
      | o = \supseteq
      | r = B \cup T
      | c = Set Union Preserves Subsets: Corollary
}}
{{eqn | ll= \leadsto
      | q = \forall T \subseteq S
      | l = T \cup A
      | o = \supseteq
      | r = T \cup B
      | c = Union is Commutative
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Hensel's Lemma/P-adic Integers/Lemma 4

:$\tuple{d_0} \in S_1$

Proof:
Let the $p$-adic expansion for $\alpha_0$ be:
:$\ds \alpha_0 = \sum_{n \mathop = 0}^\infty d_n p^n$
We have:
{{begin-eqn}}
{{eqn | l = \alpha_0 - d_0 
      | r = \paren{\sum_{n \mathop = 0}^\infty d_n p^n} - d_0
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty d_n p^n
      | c = Subtract first term from the sum
}}
{{eqn | r = p \paren{\sum_{n \mathop = 1}^\infty d_n p^{n-1} }
      | c = Factor $p$ from the sum
}}
{{eqn | o = \in
      | r = p\Z_p
}}
{{eqn | ll = \leadsto 
      | o = \equiv 
      | l = d_0 
      | r = \alpha_0
      | rr= \pmod {p\Z_p}
      | c = {{Defof|Congruence Modulo Ideal}}
}}
{{end-eqn}}
From Polynomials of Congruent Ring Elements are Congruent:
:$\map F {d_0} \equiv \map F {\alpha_0} \equiv 0 \pmod {p\Z_p}$
Hence:
:$\tuple {d_0} \in S_1$
{{qed}}
Category:Hensel's Lemma
fpibsgd23zyzle1db9n5ptd6ge9xprz
Theorem: Hensel's Lemma/P-adic Integers/Lemma 5

Let:
:$\tuple{b_0, b_1, \ldots, b_{k-1}} \in S_k$.
Then there exists a unique $p$-adic digit $\map b {b_0, b_1, \ldots, b_{k-1}}$:
:$\tuple{b_0, b_1, \ldots, b_{k-1}, \map b {b_0, b_1, \ldots, b_{k-1}}} \in S_{k+1}$

Proof:
=== Lemma 6 ===
{{:Hensel's Lemma/P-adic Integers/Lemma 6}}{{qed|lemma}}
Theorem: Hensel's Lemma/P-adic Integers/Lemma 2

:$\alpha \equiv \alpha_0 \pmod {p\Z_p}$

Proof:
From Ideals of $p$-adic Integers:
:$p \Z_p$ is an ideal of the ring $\Z_p$
By definition of congruence modulo ideal:
:$\forall k \in \N: a_k - \alpha_0 \in p \Z_p$
By definition of $p$-adic expansion:
:$\alpha = \ds \lim_{k \mathop \to \infty} a_k$
From Sum Rule for Sequences in Normed Division Ring:
:$\alpha - \alpha_0 = \ds \lim_{k \mathop \to \infty} a_k - \alpha_0$
From Closed Subgroups of $p$-adic Integers:
:$p \Z_p$ is a closed set in the $p$-adic metric
From Subset of Metric Space contains Limits of Sequences iff Closed:
:$\alpha - \alpha_0 \in p \Z_p$
By definition of congruence modulo ideal:
:$\alpha \equiv \alpha_0 \pmod {p \Z_p}$
{{qed}}
Category:Hensel's Lemma
5crcz4v07vsglq1r9dg18ytaat1fa8v
Theorem: Power Structure of Semigroup Ordered by Subsets is Ordered Semigroup

Let $\struct {S, \circ}$ be a semigroup.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Let $\struct {\powerset S, \circ_\PP, \subseteq}$ be the ordered structure formed from $\struct {\powerset S, \circ_\PP}$ and the subset relation.
Then $\struct {\powerset S, \circ_\PP, \subseteq}$ is an ordered semigroup.

Proof:
From Power Structure of Semigroup is Semigroup, $\struct {\powerset S, \circ_\PP}$ is a semigroup.
From Subset Relation is Ordering, $\struct {\powerset S, \subseteq}$ is an ordered set.
It remains to be shown that $\subseteq$ is compatible with $\circ_\PP$.
This is demonstrated directly in Subset Relation is Compatible with Subset Product.
{{qed}}
Theorem: Power Structure of Semigroup Ordered by Supersets is Ordered Semigroup

Let $\struct {S, \circ}$ be a semigroup.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Let $\struct {\powerset S, \circ_\PP, \supseteq}$ be the ordered structure formed from $\struct {\powerset S, \circ_\PP}$ and the superset relation.
Then $\struct {\powerset S, \circ_\PP, \supseteq}$ is an ordered semigroup.

Proof:
From Power Structure of Semigroup Ordered by Subsets is Ordered Semigroup, $\struct {\powerset S, \circ_\PP, \subseteq}$ is an ordered semigroup.
The result then follows from Dual of Ordered Semigroup is Ordered Semigroup.
{{qed}}
Theorem: Complement Operation between Union and Intersection Power Structures is Isomorphism

Let $S$ be a set and let $\powerset S$ be its power set.
Let $\struct {\powerset S, \cap, \subseteq}$ be the ordered semigroup formed from the set intersection operation and subset relation.
Let $\struct {\powerset S, \cap, \supseteq}$ be the ordered semigroup formed from the set intersection operation and superset relation.
Let $\struct {\powerset S, \cup, \subseteq}$ be the ordered semigroup formed from the set union operation and subset relation.
Let $\struct {\powerset S, \cup, \supseteq}$ be the ordered semigroup formed from the set union operation and superset relation.
Let $\complement: \powerset S \to \powerset S$ be the complement operation on $\powerset S$:
:$\forall X \in \powerset S: \map \complement X = S \setminus X$
where $S \setminus X$ denotes the set difference of $X$ with $S$.
Then $\complement$ is an ordered semigroup isomorphism from:
:$\struct {\powerset S, \cap, \subseteq}$ to $\struct {\powerset S, \cup, \supseteq}$
and:
:$\struct {\powerset S, \cap, \supseteq}$ to $\struct {\powerset S, \cup, \subseteq}$

Proof:
From:
:Power Set with Intersection and Subset Relation is Ordered Semigroup
:Power Set with Intersection and Superset Relation is Ordered Semigroup
:Power Set with Union and Subset Relation is Ordered Semigroup
:Power Set with Union and Superset Relation is Ordered Semigroup
each of the given ordered structures is indeed an ordered semigroup.
From Relative Complement Mapping on Powerset is Bijection, $\complement$ is a bijection.
From Relative Complement of Relative Complement it follows that $\complement$ is an involution.
From De Morgan's Laws for Relative Complements:
:$\map \complement {T_1 \cap T_2} = \map \complement {T_1} \cup \map \complement {T_2}$
and:
:$\map \complement {T_1 \cup T_2} = \map \complement {T_1} \cap \map \complement {T_2}$
hence demonstrating that $\complement$ exhibits the morphism property from both $\struct {\powerset S, \cap}$ to $\struct {\powerset S, \cup}$ and back again.
Then from Relative Complement inverts Subsets we have that $\complement$ is an order isomorphism between $\struct {\powerset S, \subseteq}$ and $\struct {\powerset S, \supseteq}$ in both directions.
Hence the result.
{{qed}}
Theorem: Non-Zero Natural Numbers under Multiplication with Divisibility forms Ordered Semigroup

Let $\N_{>0}$ be the set of natural numbers without zero, that is, $\N_{>0} = \N \setminus \set 0$.
Let $\divides$ denote the divisibility relation on $\N_{>0}$:
:$\forall a, b \in \N_{>0}: a \divides b \iff \exists k \in \Z: k \times a = b$
where $\times$ denotes conventional integer multiplication.
The ordered structure $\struct {\N_{>0}, \times, \divides}$ forms an ordered semigroup.

Proof:
First we note that from Non-Zero Natural Numbers under Multiplication form Commutative Semigroup, $\struct {\N_{>0}, \times}$ is a semigroup.
From Divisor Relation on Positive Integers is Partial Ordering, $\struct {\N_{>0}, \divides}$ is an ordered set.
It remains to be shown that $\divides$ is compatible with $\times$.
Let $a, b \in \N_{>0}$ such that $a \divides b$.
We have:
{{begin-eqn}}
{{eqn | l = a
      | o = \divides
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists k \in \Z
      | l = k \times a
      | r = b
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | ll= \leadsto
      | q = \forall m \in \N_{>0}
      | l = m \times k \times a
      | r = m \times b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = k \times \paren {m \times a}
      | r = m \times b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = m \times a
      | o = \divides
      | r = m \times b
      | c = {{Defof|Divisor of Integer}}
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = a
      | o = \divides
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists k \in \Z
      | l = k \times a
      | r = b
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | ll= \leadsto
      | q = \forall m \in \N_{>0}
      | l = k \times a \times m
      | r = b \times m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = k \times \paren {a \times m}
      | r = b \times m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a \times m
      | o = \divides
      | r = b \times m
      | c = {{Defof|Divisor of Integer}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Raw Moment of Weibull Distribution

Let $X$ be a continuous random variable with the Weibull distribution with $\alpha, \beta \in \R_{> 0}$.
Let $n$ be a strictly positive integer. 
Then the $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \beta^n \map \Gamma {1 + \dfrac n \alpha}$
where $\Gamma$ is the Gamma function.

Proof:
From the definition of the Weibull distribution, $X$ has probability density function:
:$\map {f_X} x = \alpha \beta^{-\alpha} x^{\alpha - 1} e^{-\paren {\frac x \beta}^\alpha}$
where $\Img X = \R_{\ge 0}$.
From the definition of the expected value of a continuous random variable: 
:$\ds \expect {X^n} = \int_0^\infty x^n \map {f_X} x \rd x$
Therefore:
{{begin-eqn}}
{{eqn	| l = \expect {X^n}
	    | r = \int_0^\infty x^n \alpha \beta^{-\alpha} x^{\alpha - 1} e^{-\paren {\frac x \beta}^\alpha} \rd x
}}
{{eqn	| r = \int_0^\infty x^n \dfrac \alpha \beta \paren {\dfrac x \beta}^{\alpha - 1} e^{-\paren {\frac x \beta}^\alpha} \rd x
	    | c = Rewriting
}}
{{end-eqn}}
Let: 
:$u = \paren {\dfrac x \beta}^\alpha$
Then by Chain Rule for Derivatives, we have:
:$\dfrac {\d u} {\d x} = \alpha \paren {\dfrac x \beta}^{\alpha - 1} \dfrac 1 \beta$
and also:
:$\paren {\beta u^{\frac 1 \alpha} }^n = x^n$
We can see that:
:$u \to 0$ as $x \to 0$
and
:$u \to \infty$ as $x \to \infty$
Plugging these results back into our integral above, we have:
{{begin-eqn}}
{{eqn	| l = \expect {X^n}
	    | r = \int_0^\infty \beta^n u^{\frac n \alpha} e^{-u} \rd u
}}
{{eqn	| r = \beta^n \int_0^\infty u^{\frac n \alpha + 1 - 1} e^{-u} \rd u
        | c = Linear Combination of Definite Integrals
}}
{{eqn	| r = \beta^n \map \Gamma {1 + \frac n \alpha}
        | c = {{Defof|Gamma Function}}
}}
{{end-eqn}}
{{qed}}
Category:Weibull Distribution
Category:Raw Moments
ev4lz26gvwp8x3jjh0y1m9ioyjofspo
Theorem: Expectation of Weibull Distribution

Let $X$ be a continuous random variable with the Weibull distribution with $\alpha, \beta \in \R_{> 0}$.
The expectation of $X$ is given by:
:$\expect X = \beta \, \map \Gamma {1 + \dfrac 1 \alpha}$
where $\Gamma$ is the Gamma function.

Proof:
From Raw Moment of Weibull Distribution, we have:
The $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \beta^n \map \Gamma {1 + \dfrac n \alpha}$
Therefore, for $n = 1$ we have:
:$\expect X = \beta^1 \map \Gamma {1 + \dfrac 1 \alpha}$
Hence the result.
{{qed}}
Category:Weibull Distribution
Category:Expectation
8ahjayoj6doftczsq9gp3kt94j549pm
Theorem: Variance of Weibull Distribution

Let $X$ be a continuous random variable with the Weibull distribution with $\alpha, \beta \in \R_{> 0}$.
Then the variance of $X$ is given by: 
:$\var X = \beta^2 \paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}$
where $\Gamma$ is the Gamma function.

Proof:
By Variance as Expectation of Square minus Square of Expectation, we have: 
:$\var X = \expect {X^2} - \paren {\expect X}^2$
By Expectation of Weibull Distribution, we have: 
:$\expect X = \beta \, \map \Gamma {1 + \dfrac 1 \alpha}$
From Raw Moment of Weibull Distribution, we have:
The $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \beta^n \map \Gamma {1 + \dfrac n \alpha}$
Therefore, for $n = 2$ we have:
:$\expect {X^2} = \beta^2 \map \Gamma {1 + \dfrac 2 \alpha}$
So:
{{begin-eqn}}
{{eqn	| l = \var X
	    | r = \beta^2 \map \Gamma {1 + \frac 2 \alpha} - \paren {\beta \, \map \Gamma {1 + \frac 1 \alpha} }^2
}}
{{eqn	| r = \beta^2 \paren {\map \Gamma {1 + \frac 2 \alpha} - \paren {\map \Gamma {1 + \frac 1 \alpha} }^2}
}}
{{end-eqn}}
{{qed}}
Category:Variance
Category:Weibull Distribution
keyqdktv5moha1mi7vhmc0p11os54hm
Theorem: Skewness of Weibull Distribution

Let $X$ be a continuous random variable with the Weibull distribution with $\alpha, \beta \in \R_{> 0}$.
Then the skewness $\gamma_1$ of $X$ is given by:
:$\gamma_1 = \dfrac {\map \Gamma {1 + \dfrac 3 \alpha} - 3 \map \Gamma {1 + \dfrac 1 \alpha} \map \Gamma {1 + \dfrac 2 \alpha}  + 2 \map \Gamma {1 + \dfrac 1 \alpha}^3} {\paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}^{\frac 3 2 } }$
where $\Gamma$ is the Gamma function.

Proof:
From Skewness in terms of Non-Central Moments, we have: 
:$\gamma_1 = \dfrac {\expect {X^3} - 3 \mu \sigma^2 - \mu^3} {\sigma^3}$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
By Expectation of Weibull Distribution we have: 
:$\mu = \beta \, \map \Gamma {1 + \dfrac 1 \alpha}$ 
By Variance of Weibull Distribution we have: 
:$\sigma = \beta \, \paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}^{\frac 1 2}$ 
From Raw Moment of Weibull Distribution, we have:
:$\expect {X^3} = \beta^3 \map \Gamma {1 + \dfrac 3 \alpha}$
So: 
{{begin-eqn}}
{{eqn	| l = \gamma_1
	    | r = \frac {\beta^3 \map \Gamma {1 + \dfrac 3 \alpha} - 3 \beta \, \map \Gamma {1 + \dfrac 1 \alpha} \beta^2 \paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}  - \paren {\beta \, \map \Gamma {1 + \dfrac 1 \alpha} }^3} {\paren {\beta \, \paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}^{\frac 1 2 } }^3 }
}}
{{eqn	| r = \frac {\map \Gamma {1 + \dfrac 3 \alpha} - 3 \map \Gamma {1 + \dfrac 1 \alpha} \paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}  - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^3} {\paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}^{\frac 3 2 } }
        | c = canceling $\beta^3$
}}
{{eqn	| r = \frac {\map \Gamma {1 + \dfrac 3 \alpha} - 3 \map \Gamma {1 + \dfrac 1 \alpha} \map \Gamma {1 + \dfrac 2 \alpha}  + 2 \map \Gamma {1 + \dfrac 1 \alpha}^3} {\paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}^{\frac 3 2 } }
        | c = 
}}
{{end-eqn}}
{{qed}}
Category:Skewness
Category:Weibull Distribution
c40vi6roohyaudpg3a0ekv6stg5gyxu
Theorem: Inverse of Infimum in Ordered Group is Supremum of Inverses

Let $\struct {G, \circ, \preccurlyeq}$ be an ordered group.
Let $x, y \in G$.
Then:
:$\set {x, y}$ admits an infimum in $G$
{{iff}}:
:$\set {x^{-1}, y^{-1} }$ admits a supremum in $G$
in which case:
:$\paren {\inf \set {x, y} }^{-1} = \sup \set {x^{-1}, y^{-1} }$

Proof:
=== Sufficient Condition ===
Let $\set {x, y}$ admits an infimum $c$ in $G$.
Then:
{{begin-eqn}}
{{eqn | l = c
      | o = \preccurlyeq
      | r = x
      | c = as $c$ is a lower bound of $\set {x, y}$
}}
{{eqn | lo= \land
      | l = c
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^{-1}
      | o = \preccurlyeq
      | r = c^{-1}
      | c = Inversion Mapping Reverses Ordering in Ordered Group
}}
{{eqn | lo= \land
      | l = y^{-1}
      | o = \preccurlyeq
      | r = c^{-1}
      | c = 
}}
{{end-eqn}}
and so $c^{-1}$ is an upper bound of $\set {x^{-1}, y^{-1} }$.
Suppose $d$ is an upper bound of $\set {x^{-1}, y^{-1} }$.
Then:
{{begin-eqn}}
{{eqn | l = x^{-1}
      | o = \preccurlyeq
      | r = d
      | c = {{Defof|Upper Bound of Set}}
}}
{{eqn | lo= \land
      | l = y^{-1}
      | o = \preccurlyeq
      | r = d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d^{-1}
      | o = \preccurlyeq
      | r = x
      | c = Inversion Mapping Reverses Ordering in Ordered Group
}}
{{eqn | lo= \land
      | l = d^{-1}
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{end-eqn}}
That is, $d^{-1}$ is a lower bound of $\set {x, y}$.
But because $c$ is an infimum of $\set {x, y}$:
{{begin-eqn}}
{{eqn | l = c
      | o = \preccurlyeq
      | r = d^{-1}
      | c = {{Defof|Infimum of Set}}
}}
{{eqn | ll= \leadsto
      | l = c^{-1}
      | o = \preccurlyeq
      | r = d
      | c = Inversion Mapping Reverses Ordering in Ordered Group
}}
{{end-eqn}}
That is, for an arbitrary upper bound $d$ of $\set {x^{-1}, y^{-1} }$:
:$c^{-1} \preccurlyeq d$
and so $c^{-1}$ is a supremum of $\set {x^{-1}, y^{-1} }$ by definition.
That is:
:$\paren {\inf \set {x, y} }^{-1} = \sup \set {x^{-1}, y^{-1} }$
{{qed|lemma}}
Theorem: Inverse of Supremum in Ordered Group is Infimum of Inverses

Let $\struct {G, \circ, \preccurlyeq}$ be an ordered group.
Let $x, y \in G$.
Then:
:$\set {x, y}$ admits a supremum in $G$
{{iff}}:
:$\set {x^{-1}, y^{-1} }$ admits an infimum in $G$
in which case:
:$\paren {\sup \set {x, y} }^{-1} = \inf \set {x^{-1}, y^{-1} }$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = a
      | r = x^{-1}
}}
{{eqn | l = b
      | r = y^{-1}
}}
{{end-eqn}}
Recall from Inverse of Group Inverse:
{{begin-eqn}}
{{eqn | l = a^{-1}
      | r = x
}}
{{eqn | l = b^{-1}
      | r = y
}}
{{end-eqn}}
From Inverse of Infimum in Ordered Group is Supremum of Inverses:
Then:
:$\set {a, b}$ admits an infimum in $G$
{{iff}}:
:$\set {a^{-1}, b^{-1} }$ admits a supremum in $G$
in which case:
:$\paren {\inf \set {a, b} }^{-1} = \sup \set {a^{-1}, b^{-1} }$
Substituting back for $a$ and $b$:
:$\set {x^{-1}, y^{-1} }$ admits an infimum in $G$
{{iff}}:
:$\set {x, y}$ admits a supremum in $G$
in which case:
:$\paren {\inf \set {x^{-1}, x^{-1} } }^{-1} = \sup \set {x, y}$
Hence from {{Group-axiom|3}}: 
:$\inf \set {x^{-1}, x^{-1} } = \paren {\sup \set {x, y} }^{-1}$
{{qed}}
Theorem: Product of Supremum and Infimum in Lattice-Ordered Group

Let $\struct {G, \odot}$ be a group.
Let $\preccurlyeq$ be a lattice ordering on $G$.
Let $x, y \in G$ such that $x$ commutes with $y$.
Then:
:$\sup \set {x, y} \odot \inf \set {x, y} = x \odot y$

Proof:
First we show that $x$ commutes with $\sup \set {x, y}$.
Indeed:
{{begin-eqn}}
{{eqn | l = x \odot \sup \set {x, y}
      | r = \sup \set {x \odot x, x \odot y}
      | c = Suprema in Ordered Group
}}
{{eqn | r = \sup \set {x \odot x, y \odot x}
      | c = as $x$ and $y$ commute
}}
{{eqn | r = \sup \set {x, y} \odot x
      | c = Suprema in Ordered Group
}}
{{end-eqn}}
Similarly:
:$y$ commutes with $\sup \set {x, y}$
Then using Infima in Ordered Group in the same way as above:
:$x$ commutes with $\inf \set {x, y}$
:$y$ commutes with $\inf \set {x, y}$
Then we have:
{{begin-eqn}}
{{eqn | l = x \odot \paren {\sup \set {x, y} }^{-1} \odot y
      | r = x \odot \inf \set {x^{-1}, y^{-1} } \odot y
      | c = 
}}
{{eqn | r = \inf \set {x \odot x^{-1} \odot y, x \odot y^{-1} \odot y}
      | c = Inverse of Supremum in Ordered Group is Infimum of Inverses
}}
{{eqn | r = \inf \set {y, x}
      | c = 
}}
{{eqn | r = \inf \set {x, y}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \odot y \odot \paren {\sup \set {x, y} }^{-1}
      | r = \inf \set {x, y}
      | c = from the commutativity proved {{apriori}}
}}
{{eqn | ll= \leadsto
      | l = x \odot y
      | r = \sup \set {x, y} \odot \inf \set {x, y}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Ordered Group whose Doubletons with Identity admit Supremum is Lattice

Let $\struct {G, \odot, \preccurlyeq}$ be an ordered group whose identity element is $e$.
Let $\preccurlyeq$ be such that for all $x \in G$, $\set {x, e}$ admits a supremum.
Then $\preccurlyeq$ is a lattice ordering.

Proof:
Let $x, y \in G$ be arbitrary.
We have that $y = x \odot z$ for some $z \in G$.
From Suprema in Ordered Group:
:$\set {z, e}$ admits a supremum {{iff}} $\set {x \odot z, x \odot e}$ admits a supremum.
It follows that:
:$\set {x, y}$ admits a supremum.
As $x$ and $y$ are arbitrary, it follows that:
:$\forall x, y \in G: \set {x, y}$ admits a supremum.
Let $x = a^{-1}$ and $y = b^{-1}$.
That is:
:$a = x^{-1}$ and $b = y^{-1}$
Thus we have that:
:$\set {a, b}$ admits a supremum.
From Inverse of Supremum in Ordered Group is Infimum of Inverses it follows directly that:
:$\set {a^{-1}, b^{-1} }$ admits an infimum
from which:
:$\set {x, y}$ admits an infimum.
As $x$ and $y$ are arbitrary, we have that:
:$\forall x, y \in G: \set {x, y}$ admits both a supremum and an infimum,
The result follows by definition of lattice ordering.
{{qed}}