IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory OrderedLoop_ZF imports Loop_ZF Fold_ZF

begin

This theory file is about properties of loops (the algebraic structures introduced in IsarMathLib in the Loop_ZF theory) with an additional order relation that is in a way compatible with the loop's binary operation. The oldest reference I have found on the subject is \cite{Zelinski1948}.

Definition, notation and basic properties

An ordered loop \((G,A)\) is a loop with a partial order relation r that is "translation invariant" with respect to the loop operation \(A\).

A triple \((G,A,r)\) is an ordered loop if \((G,A)\) is a loop and \(r\) is a relation on \(G\) (i.e. a subset of \(G\times G\) with is a partial order and for all elements \(x,y,z \in G\) the condition \(\langle x,y\rangle \in r\) is equivalent to both \(\langle A\langle x,z\rangle, A\langle x,z\rangle\rangle \in r\) and \(\langle A\langle z,x\rangle, A\langle z,x\rangle\rangle \in r\). This looks a bit awkward in the basic set theory notation, but using the additive notation for the group operation and \(x\leq y\) to instead of \(\langle x,y \rangle \in r\) this just means that \(x\leq y\) if and only if \(x+z\leq y+z\) and \(x\leq y\) if and only if \(z+x\leq z+y\).

definition

\( \text{IsAnOrdLoop}(L,A,r) \equiv \) \( \text{IsAloop}(L,A) \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \forall z\in L.\ \) \( ((\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ))) \)

We define the set of nonnegative elements in the obvious way as \(L^+ =\{x\in L: 0 \leq x\}\).

definition

\( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)

The \( \text{PositiveSet}(L,A,r) \) is a set similar to \( \text{Nonnegative}(L,A,r) \), but without the neutral element. What we call the positive set here is sometimes called "the positive cone" of an ordered loop.

definition

\( \text{PositiveSet}(L,A,r) \equiv \) \( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} \)

An ordered loop may satisfy the following condition: for every \(b_1 > 0\) there is a \(b_2 > 0\) such that \(b_2 + b_2 \leq b_1 \). This condition is needed as an assumption in a couple of places. I don't think there is a standard name for this property (please let me know if there is one), we will use the name IsHalfable here.

definition

\( \text{IsHalfable}(L,A,r) \equiv \forall b_1\in \text{PositiveSet}(L,A,r).\ \exists b_2\in \text{PositiveSet}(L,A,r).\ \langle A\langle b_2,b_2\rangle ,b_1\rangle \in r \)

We will use the additive notation for ordered loops.

locale loop1

assumes ordLoopAssum: \( \text{IsAnOrdLoop}(L,A,r) \)

defines \( 0 \equiv \text{ TheNeutralElement}(L,A) \)

defines \( x + y \equiv A\langle x,y\rangle \)

defines \( x \leq y \equiv \langle x,y\rangle \in r \)

defines \( x \lt y \equiv x\leq y \wedge x\neq y \)

defines \( L^+ \equiv \text{Nonnegative}(L,A,r) \)

defines \( L_+ \equiv \text{PositiveSet}(L,A,r) \)

defines \( - x + y \equiv \text{ LeftDiv}(L,A)\langle x,y\rangle \)

defines \( x - y \equiv \text{ RightDiv}(L,A)\langle y,x\rangle \)

defines \( \sum s \equiv \text{Fold}(A, 0 ,s) \)

defines \( n\cdot x \equiv \sum \{\langle k,x\rangle .\ k\in n\} \)

Theorems proven in the loop0 locale are valid in the loop1 locale

sublocale loop1 < loop0

using ordLoopAssum, loop_loop0_valid unfolding IsAnOrdLoop_def

The notation \(-x+y\) and \(x-y\) denotes left and right division, resp. These two operations are closed in a loop, see lemma lrdiv_binop in the Quasigroup_ZF theory. The next lemma reiterates that fact using the notation of the loop1 context.

lemma (in loop1) left_right_sub_closed:

assumes \( x\in L \), \( y\in L \)

shows \( ( - x + y) \in L \) and \( x - y \in L \)proof

from qgroupassum have \( \text{ LeftDiv}(L,A):L\times L \rightarrow L \) and \( \text{ RightDiv}(L,A):L\times L \rightarrow L \) using lrdiv_binop

with assms show \( ( - x + y) \in L \) and \( x - y \in L \) using apply_funtype

qed

In this context \(x \leq y\) implies that both \(x\) and \(y\) belong to \(L\).

lemma (in loop1) lsq_members:

assumes \( x\leq y \)

shows \( x\in L \) and \( y\in L \) using ordLoopAssum, assms, IsAnOrdLoop_def

In this context \(x < y\) implies that both \(x\) and \(y\) belong to \(L\).

lemma (in loop1) less_members:

assumes \( x \lt y \)

shows \( x\in L \) and \( y\in L \) using ordLoopAssum, assms, IsAnOrdLoop_def

In an ordered loop the order is translation invariant.

lemma (in loop1) ord_trans_inv:

assumes \( x\leq y \), \( z\in L \)

shows \( x + z \leq y + z \) and \( z + x \leq z + y \)proof

from ordLoopAssum, assms have \( (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ) \) using lsq_members unfolding IsAnOrdLoop_def

with assms(1) show \( x + z \leq y + z \) and \( z + x \leq z + y \)

qed

In an ordered loop the strict order is translation invariant.

lemma (in loop1) strict_ord_trans_inv:

assumes \( x \lt y \), \( z\in L \)

shows \( x + z \lt y + z \) and \( z + x \lt z + y \)proof

from assms have \( x + z \leq y + z \) and \( z + x \leq z + y \) using ord_trans_inv

moreover

have \( x + z \neq y + z \) and \( z + x \neq z + y \)proof

{

assume \( x + z = y + z \)

with assms have \( x=y \) using less_members, qg_cancel_right

with assms(1) have \( False \)

}

thus \( x + z \neq y + z \)

{

assume \( z + x = z + y \)

with assms have \( x=y \) using less_members, qg_cancel_left

with assms(1) have \( False \)

}

thus \( z + x \neq z + y \)

qed

ultimately show \( x + z \lt y + z \) and \( z + x \lt z + y \)

qed

We can cancel an element from both sides of an inequality on the right side.

lemma (in loop1) ineq_cancel_right:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( x + z \leq y + z \)

shows \( x\leq y \)proof

from ordLoopAssum, assms(1,2,3) have \( \langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r \) unfolding IsAnOrdLoop_def

with assms(4) show \( x\leq y \)

qed

We can cancel an element from both sides of a strict inequality on the right side.

lemma (in loop1) strict_ineq_cancel_right:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( x + z \lt y + z \)

shows \( x \lt y \) using assms, ineq_cancel_right

We can cancel an element from both sides of an inequality on the left side.

lemma (in loop1) ineq_cancel_left:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \leq z + y \)

shows \( x\leq y \)proof

from ordLoopAssum, assms(1,2,3) have \( \langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r \) unfolding IsAnOrdLoop_def

with assms(4) show \( x\leq y \)

qed

We can cancel an element from both sides of a strict inequality on the left side.

lemma (in loop1) strict_ineq_cancel_left:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \lt z + y \)

shows \( x \lt y \) using assms, ineq_cancel_left

We can subtract a loop element from both sides of inequality both on the left side and right.

lemma (in loop1) ineq_subtr_from_sides:

assumes \( x\leq y \), \( z\in L \)

shows \( x - z \leq y - z \) and \( ( - z + x) \leq - z + y \)proof

from assms have T: \( x - z\in L \), \( y - z\in L \), \( ( - z + x)\in L \), \( ( - z + y)\in L \) and \( x = (x - z) + z \), \( y = (y - z) + z \) and \( x = z + ( - z + x) \), \( y = z + ( - z + y) \) using lsq_members, lrdiv_props(2,3,5,6)

with assms(1) have \( (x - z) + z \leq (y - z) + z \) and \( z + ( - z + x) \leq z + ( - z + y) \)

with assms(2), T show \( x - z \leq y - z \) and \( ( - z + x) \leq - z + y \) using ineq_cancel_left, ineq_cancel_right

qed

We can subtract a loop element from both sides of of a strict inequality both on the left side and right.

lemma (in loop1) strict_ineq_subtr:

assumes \( x \lt y \), \( z\in L \)

shows \( x - z \lt y - z \) and \( ( - z + x) \lt - z + y \)proof

with assms(1) have \( (x - z) + z \lt (y - z) + z \) and \( z + ( - z + x) \lt z + ( - z + y) \)

with assms(2), T show \( x - z \lt y - z \) and \( ( - z + x) \lt - z + y \) using strict_ineq_cancel_left, strict_ineq_cancel_right

qed

We can move an element to the other side of a strict inequality with three loop elements - right side variant.

lemma (in loop1) strict_ineq_move_side_right:

assumes \( x\in L \), \( y\in L \), \( x + y \lt z \)

shows \( x \lt z - y \)proof

from assms(2,3) have \( (x + y) - y \lt z - y \) using strict_ineq_subtr

with assms(1,2) show \( x \lt z - y \) using lrdiv_ident(1)

qed

We can move an element to the other side of an inequality with three loop elements - right side variant.

lemma (in loop1) ineq_move_side_right:

assumes \( x\in L \), \( y\in L \), \( x + y\leq z \)

shows \( x\leq z - y \) using assms, ineq_subtr_from_sides(1), lrdiv_ident(1)

We can move \(y\) to the other side of an inequality \(z\leq x+y\).

lemma (in loop1) ineq_move_side_right1:

assumes \( x\in L \), \( y\in L \), \( z\leq x + y \)

shows \( z - y\leq x \) using assms, ineq_subtr_from_sides(1), lrdiv_ident(1)

We can move an element to the other side of an inequality with three loop elements - left side variant.

lemma (in loop1) ineq_move_side_left:

assumes \( x\in L \), \( y\in L \), \( x + y\leq z \)

shows \( y \leq - x + z \) using assms, ineq_subtr_from_sides(2), lrdiv_ident(2)

We can move \(x\) to the other side of an inequality \(z\leq x+y\).

lemma (in loop1) ineq_move_side_left1:

assumes \( x\in L \), \( y\in L \), \( z\leq x + y \)

shows \( ( - x + z) \leq y \) using assms, ineq_subtr_from_sides(2), lrdiv_ident(2)

The definition of the nonnegative set in the notation used in the loop1 locale:

lemma (in loop1) nonneg_definition:

shows \( x \in L^+ \longleftrightarrow 0 \leq x \) using ordLoopAssum, IsAnOrdLoop_def, Nonnegative_def

The nonnegative set is contained in the loop.

lemma (in loop1) nonneg_subset:

shows \( L^+ \subseteq L \) using Nonnegative_def

The positive set is contained in the loop.

lemma (in loop1) positive_subset:

shows \( L_+ \subseteq L \) using PositiveSet_def

The definition of the positive set in the notation used in the loop1 locale:

lemma (in loop1) posset_definition:

shows \( x \in L_+ \longleftrightarrow ( 0 \leq x \wedge x\neq 0 ) \) using ordLoopAssum, IsAnOrdLoop_def, PositiveSet_def

Another form of the definition of the positive set in the notation used in the loop1 locale:

lemma (in loop1) posset_definition1:

shows \( x \in L_+ \longleftrightarrow 0 \lt x \) using ordLoopAssum, IsAnOrdLoop_def, PositiveSet_def

The order in an ordered loop is antisymmeric.

lemma (in loop1) loop_ord_antisym:

assumes \( x\leq y \) and \( y\leq x \)

shows \( x=y \)proof

from ordLoopAssum, assms have \( \text{antisym}(r) \), \( \langle x,y\rangle \in r \), \( \langle y,x\rangle \in r \) unfolding IsAnOrdLoop_def, IsPartOrder_def

then show \( x=y \) by (rule Fol1_L4 )

qed

The loop order is transitive.

lemma (in loop1) loop_ord_trans:

assumes \( x\leq y \) and \( y\leq z \)

shows \( x\leq z \)proof

from ordLoopAssum, assms have \( \text{trans}(r) \) and \( \langle x,y\rangle \in r \wedge \langle y,z\rangle \in r \) unfolding IsAnOrdLoop_def, IsPartOrder_def

then have \( \langle x,z\rangle \in r \) by (rule Fol1_L3 )

thus \( thesis \)

qed

The loop order is reflexive.

lemma (in loop1) loop_ord_refl:

assumes \( x\in L \)

shows \( x\leq x \) using assms, ordLoopAssum unfolding IsAnOrdLoop_def, IsPartOrder_def, refl_def

The neutral element is nonnegative.

lemma (in loop1) loop_zero_nonneg:

shows \( 0 \in L^+ \) using neut_props_loop(1), loop_ord_refl, nonneg_definition

A form of mixed transitivity for the strict order:

lemma (in loop1) loop_strict_ord_trans:

assumes \( x\leq y \) and \( y \lt z \)

shows \( x \lt z \)proof

from assms have \( x\leq y \) and \( y\leq z \)

then have \( x\leq z \) by (rule loop_ord_trans )

with assms show \( x \lt z \) using loop_ord_antisym

qed

Another form of mixed transitivity for the strict order:

lemma (in loop1) loop_strict_ord_trans1:

assumes \( x \lt y \) and \( y\leq z \)

shows \( x \lt z \)proof

from assms have \( x\leq y \) and \( y\leq z \)

then have \( x\leq z \) by (rule loop_ord_trans )

with assms show \( x \lt z \) using loop_ord_antisym

qed

Yet another form of mixed transitivity for the strict order:

lemma (in loop1) loop_strict_ord_trans2:

assumes \( x \lt y \) and \( y \lt z \)

shows \( x \lt z \)proof

from assms have \( x\leq y \) and \( y\leq z \)

then have \( x\leq z \) by (rule loop_ord_trans )

with assms show \( x \lt z \) using loop_ord_antisym

qed

We can move an element to the other side of an inequality. Well, not exactly, but our notation creates an illusion to that effect.

lemma (in loop1) lsq_other_side:

assumes \( x\leq y \)

shows \( 0 \leq - x + y \), \( ( - x + y) \in L^+ \), \( 0 \leq y - x \), \( (y - x) \in L^+ \)proof

from assms have \( x\in L \), \( y\in L \), \( 0 \in L \), \( ( - x + y) \in L \), \( (y - x) \in L \) using lsq_members, neut_props_loop(1), lrdiv_props(2,5)

then have \( x = x + 0 \) and \( y = x + ( - x + y) \) using neut_props_loop(2), lrdiv_props(6)

with assms have \( x + 0 \leq x + ( - x + y) \)

with \( x\in L \), \( 0 \in L \), \( ( - x + y) \in L \) show \( 0 \leq - x + y \) using ineq_cancel_left

then show \( ( - x + y) \in L^+ \) using nonneg_definition

from \( x\in L \), \( y\in L \) have \( x = 0 + x \) and \( y = (y - x) + x \) using neut_props_loop(2), lrdiv_props(3)

with assms have \( 0 + x \leq (y - x) + x \)

with \( x\in L \), \( 0 \in L \), \( (y - x) \in L \) show \( 0 \leq y - x \) using ineq_cancel_right

then show \( (y - x) \in L^+ \) using nonneg_definition

qed

We can move an element to the other side of a strict inequality.

lemma (in loop1) ls_other_side:

assumes \( x \lt y \)

shows \( 0 \lt - x + y \), \( ( - x + y) \in L_+ \), \( 0 \lt y - x \), \( (y - x) \in L_+ \)proof

from assms have \( x\in L \), \( y\in L \), \( 0 \in L \), \( ( - x + y) \in L \), \( (y - x) \in L \) using lsq_members, neut_props_loop(1), lrdiv_props(2,5)

then have \( x = x + 0 \) and \( y = x + ( - x + y) \) using neut_props_loop(2), lrdiv_props(6)

with assms have \( x + 0 \lt x + ( - x + y) \)

with \( x\in L \), \( 0 \in L \), \( ( - x + y) \in L \) show \( 0 \lt - x + y \) using strict_ineq_cancel_left

then show \( ( - x + y) \in L_+ \) using posset_definition1

from \( x\in L \), \( y\in L \) have \( x = 0 + x \) and \( y = (y - x) + x \) using neut_props_loop(2), lrdiv_props(3)

with assms have \( 0 + x \lt (y - x) + x \)

with \( x\in L \), \( 0 \in L \), \( (y - x) \in L \) show \( 0 \lt y - x \) using strict_ineq_cancel_right

then show \( (y - x) \in L_+ \) using posset_definition1

qed

We can add sides of inequalities.

lemma (in loop1) add_ineq:

assumes \( x\leq y \), \( z\leq t \)

shows \( x + z \leq y + t \)proof

from assms have \( x + z \leq y + z \) using lsq_members(1), ord_trans_inv(1)

with assms show \( thesis \) using lsq_members(2), ord_trans_inv(2), loop_ord_trans

qed

We can add sides of strict inequalities. The proof uses a lemma that relies on the antisymmetry of the order relation.

lemma (in loop1) add_ineq_strict:

assumes \( x \lt y \), \( z \lt t \)

shows \( x + z \lt y + t \)proof

from assms have \( x + z \lt y + z \) using less_members(1), strict_ord_trans_inv(1)

moreover

from assms have \( y + z \lt y + t \) using less_members(2), strict_ord_trans_inv(2)

ultimately show \( thesis \) by (rule loop_strict_ord_trans2 )

qed

We can add sides of inequalities one of which is strict.

lemma (in loop1) add_ineq_strict1:

assumes \( x\leq y \), \( z \lt t \)

shows \( x + z \lt y + t \) and \( z + x \lt t + y \)proof

from assms have \( x + z \leq y + z \) using less_members(1), ord_trans_inv(1)

with assms show \( x + z \lt y + t \) using lsq_members(2), strict_ord_trans_inv(2), loop_strict_ord_trans

from assms have \( z + x \lt t + x \) using lsq_members(1), strict_ord_trans_inv(1)

with assms show \( z + x \lt t + y \) using less_members(2), ord_trans_inv(2), loop_strict_ord_trans1

qed

Subtracting a positive element decreases the value, while adding a positive element increases the value.

lemma (in loop1) add_subtract_pos:

assumes \( x\in L \), \( 0 \lt y \)

shows \( x - y \lt x \), \( ( - y + x) \lt x \), \( x \lt x + y \), \( x \lt y + x \)proof

from assms(2) have \( y\in L \) using less_members(2)

from assms(1) have \( x\leq x \) using ordLoopAssum unfolding IsAnOrdLoop_def, IsPartOrder_def, refl_def

with assms(2) have \( x + 0 \lt x + y \) using add_ineq_strict1(1)

with assms, \( y\in L \) show \( x - y \lt x \) using neut_props_loop(2), lrdiv_props(3), lrdiv_props(2), strict_ineq_cancel_right

from assms(2), \( x\leq x \) have \( 0 + x \lt y + x \) using add_ineq_strict1(2)

with assms, \( y\in L \) show \( ( - y + x) \lt x \) using neut_props_loop(2), lrdiv_props(6), lrdiv_props(5), strict_ineq_cancel_left

from assms(1), \( x + 0 \lt x + y \), \( 0 + x \lt y + x \) show \( x \lt x + y \), \( x \lt y + x \) using neut_props_loop(2)

qed

The set of nonnegative elements is closed under the loop operation.

lemma (in loop1) nonneg_closed:

shows \( L^+ \text{ is closed under } A \)proof

{

fix \( x \) \( y \)

assume \( x\in L^+ \), \( y\in L^+ \)

then have \( x + y \in L^+ \) using nonneg_definition, add_ineq, neut_props_loop

}

then show \( L^+ \text{ is closed under } A \) unfolding IsOpClosed_def

qed

The sum of a list of nonnegative elements of a loop is nonnegative.

lemma (in loop1) sum_nonneg_nonneg:

assumes \( n\in nat \), \( s:n\rightarrow L^+ \)

shows \( (\sum s) \in L^+ \) using ordLoopAssum, assms, nonneg_subset, loop_zero_nonneg, nonneg_closed, fold_in_op_closed unfolding IsAnOrdLoop_def, IsAloop_def, IsAquasigroup_def

In an ordered loop if the order relation down-directs the set of positive elements \(L_+\) then \(L_+\) is a down-directed set (see Order_ZF for definitions of those related but different notions).

lemma (in loop1) down_directs_directed:

assumes \( r \text{ down-directs } L_+ \)

shows \( \text{IsDownDirectedSet}(L_+,r) \) using ordLoopAssum, assms, positive_subset, down_directs_subset unfolding IsAnOrdLoop_def

Each nonempty set of nonnegative loop elements is bounded below.

lemma (in loop1) nonnegative_bounded_below:

assumes \( B\subseteq L^+ \)

shows \( \text{IsBoundedBelow}(B,r) \)proof

{

fix \( x \)

assume \( x\in B \)

with assms have \( x\in \text{Nonnegative}(L,A,r) \)

}

then show \( \text{IsBoundedBelow}(B,r) \) unfolding Nonnegative_def, IsBoundedBelow_def

qed

If a set of nonnegative group grpup elements has an infimum, then that infimum is nonnegative.

lemma (in loop1) inf_nonneg_nonneg:

assumes \( B\subseteq L^+ \) and \( \text{HasAnInfimum}(r,B) \)

shows \( \text{Infimum}(r,B) \in L^+ \)proof

from assms(1) have \( \forall x\in B.\ 0 \leq x \) using nonneg_definition

with ordLoopAssum, assms show \( \text{Infimum}(r,B) \in L^+ \) using inf_geq_lo_bnd, nonneg_definition unfolding IsAnOrdLoop_def, IsPartOrder_def

qed

If \(0\) is an element of a subset of nonnegative elements, then that subset has a minimum and infimum, both equal to \(0\).

lemma (in loop1) zero_subset_nneg:

assumes \( B\subseteq L^+ \), \( 0 \in B \)

shows \( \text{HasAminimum}(r,B) \), \( \text{Minimum}(r,B) = 0 \) and \( \text{HasAnInfimum}(r,B) \), \( \text{Infimum}(r,B) = 0 \)proof

from assms(1) have \( \forall x\in B.\ 0 \leq x \) using nonneg_definition

with ordLoopAssum, assms show \( \text{HasAminimum}(r,B) \), \( \text{Minimum}(r,B) = 0 \) and \( \text{HasAnInfimum}(r,B) \), \( \text{Infimum}(r,B) = 0 \) using Order_ZF_4_L15, min_is_inf unfolding IsAnOrdLoop_def, IsPartOrder_def

qed

Completness vs Archimedean property

For ordered fields the completeness of the order implies the Archimedean property: for every two positive elements there is a natural number \(n\) such that \(y < n x\). In 1891 Otto Stolz "succeeded in proving that the positive cone of a Dedekind complete ordered abelian group is Archimedean". In this section we consider the relation between the completeness of the order and the Archimedean property of the positive set of an ordered loop (not necessarily abelian).

Multiples of a positive element are positive.

lemma (in loop1) mults_pos_pos:

assumes \( 0 \lt x \), \( n\in nat\setminus \{0\} \)

shows \( 0 \lt n\cdot x \)proof

from assms(1) have \( x\in L \) using less_members(2)

{

fix \( m \)

assume \( m\in nat \)

from \( x\in L \) have \( (0 + 1)\cdot x = 0\cdot x + x \) using loop_pow_mult_one

with assms(1), \( x\in L \) have \( 0 \lt (0 + 1)\cdot x \) using loop_zero_pow, neut_props_loop(2)

{

fix \( j \)

assume \( j\in nat \) and \( 0 \lt (j + 1)\cdot x \)

from \( x\in L \) have I: \( (j + 1 + 1)\cdot x = (j + 1)\cdot x + x \) using loop_pow_mult_one

from assms(1), \( x\in L \), \( j\in nat \) have \( (j + 1)\cdot x \lt (j + 1)\cdot x + x \) using loop_prod_type, add_subtract_pos(3)

with I have \( (j + 1)\cdot x \lt (j + 1 + 1)\cdot x \)

with \( 0 \lt (j + 1)\cdot x \) have \( 0 \lt (j + 1 + 1)\cdot x \) using loop_strict_ord_trans2

}

hence \( \forall j\in nat.\ 0 \lt (j + 1)\cdot x \longrightarrow 0 \lt (j + 1 + 1)\cdot x \)

with \( m\in nat \), \( 0 \lt (0 + 1)\cdot x \) have \( 0 \lt (m + 1)\cdot x \) by (rule ind_on_nat1 )

}

hence \( \forall m\in nat.\ 0 \lt (m + 1)\cdot x \)

with assms(2) show \( 0 \lt n\cdot x \) using nat_not0_succ

qed

If the order is complete and \(x\) is a positive element of an ordered loop, then the set \(\{n\cdot x: n\in \mathbb{N}, n\neq 0\}\) is not bounded above.

lemma (in loop1) nat_mult_not_bounded:

assumes \( r \text{ is complete } \) and \( 0 \lt x \)

shows \( \neg \text{IsBoundedAbove}(\{n\cdot x.\ n\in nat\setminus \{0\}\},r) \)proof

let \( M = \{n\cdot x.\ n\in nat\setminus \{0\}\} \)

{

assume C: \( \text{IsBoundedAbove}(M,r) \)

let \( S = \text{Supremum}(r,M) \)

from ordLoopAssum, assms(1) have I: \( r\subseteq L\times L \), \( \text{antisym}(r) \), \( r \text{ is complete } \), \( M\neq \emptyset \) using loop_not_empty unfolding IsAnOrdLoop_def, IsPartOrder_def

from I, C have \( S\in L \) using compl_bounded_sup_props(1)

from I, C have \( \forall y\in M.\ \langle y,S\rangle \in r \) by (rule compl_bounded_sup_props )

hence II: \( \forall n\in nat\setminus \{0\}.\ n\cdot x\leq S \)

{

fix \( n \)

assume \( n\in nat\setminus \{0\} \)

then have \( n + 1 \in nat\setminus \{0\} \)

with assms(2), II, \( n\in nat\setminus \{0\} \) have \( n\cdot x\leq S - x \) using less_members(2), loop_pow_mult_one, loop_prod_type, ineq_move_side_right

}

hence \( \forall y\in M.\ \langle y,S - x\rangle \in r \)

with \( \text{antisym}(r) \), assms(1), \( M\neq \emptyset \) have \( \langle S,S - x\rangle \in r \) by (rule compl_sup_leq_up_bnd )

hence \( S\leq S - x \)

from assms(2), \( S\in L \) have \( S - x \lt S \) using add_subtract_pos(1)

with \( S\leq S - x \) have \( False \) using loop_strict_ord_trans

}

thus \( thesis \)

qed

We say that a nonempty subset \(A\) of a ordered loop is Archimedean if for any two elements \(x,y\) of \(A\) there is a non-zero natural number \(n\) such that \(n\cdot x\) exceeds \(y\).

definition (in loop1)

\( B \text{ is Archimedean } \equiv B\neq \emptyset \wedge (\forall x\in B.\ \forall y\in B.\ \exists n\in nat\setminus \{0\}.\ y \lt n\cdot x) \)

If the order of the loop is complete and total on the positive set, then the positive set is Archimedean.

theorem (in loop1) loop_pos_set_archimedean:

assumes \( L_+\neq \emptyset \), \( r \text{ is complete } \) and \( r \text{ is total on } L_+ \)

shows \( L_+ \text{ is Archimedean } \)proof

{

fix \( x \) \( y \)

assume \( x\in L_+ \), \( y\in L_+ \)

then have \( 0 \lt x \) and \( y\in L \) using posset_definition1, positive_subset

let \( M = \{n\cdot x.\ n\in nat\setminus \{0\}\} \)

from assms(1,2), \( 0 \lt x \) have \( \neg (\exists u.\ \forall z\in M.\ z\leq u) \) using nat_mult_not_bounded, IsBoundedAbove_def

then obtain \( z \) where \( z\in M \) and \( \neg (z\leq y) \)

from \( z\in M \) obtain \( n \) where \( n\in nat\setminus \{0\} \) and \( z=n\cdot x \)

from \( z=n\cdot x \), \( \neg (z\leq y) \) have \( \neg (n\cdot x\leq y) \)

from \( 0 \lt x \), \( n\in nat\setminus \{0\} \) have \( n\cdot x \in L_+ \) using mults_pos_pos, posset_definition

with assms(3), \( y\in L_+ \), \( \neg (n\cdot x\leq y) \), \( n\in nat\setminus \{0\} \) have \( \exists n\in nat\setminus \{0\}.\ y \lt n\cdot x \) unfolding IsTotal_def

}

with assms(1) show \( L_+ \text{ is Archimedean } \) unfolding IsArchimedean_def

qed

Suprema and infima of sets in ordered loop

The goal of this section is to show that if two sets have suprema (or infima) then the Minkowski's sum of \(A,B\) (i.e. the set \(\{x+y: x\in A, y\in B\}\) also has a supremum (or infimum) equal to \(\sup (A) + \sup (B)\) (or \(\inf (A) + \inf(B))\).)

A set that has a supremum with respect to loop order relation is a subset of the loop and the supremum is a member of the loop.

lemma (in loop1) loop_has_sup_subset:

assumes \( \text{HasAsupremum}(r,B) \)

shows \( B\subseteq L \) and \( \text{Supremum}(r,B) \in L \)proof

from ordLoopAssum, assms show \( B\subseteq L \) using has_sup_subset unfolding IsAnOrdLoop_def, IsPartOrder_def

from ordLoopAssum, assms show \( \text{Supremum}(r,B) \in L \) using set_sup_not_empty, sup_is_ub, lsq_members unfolding IsAnOrdLoop_def, IsPartOrder_def

qed

A set that has an infimum with respect to loop order relation is a subset of the loop and the infimum is a member of the loop.

lemma (in loop1) loop_has_inf_subset:

assumes \( \text{HasAnInfimum}(r,B) \)

shows \( B\subseteq L \) and \( \text{Infimum}(r,B) \in L \)proof

from ordLoopAssum, assms show \( B\subseteq L \) using has_inf_subset unfolding IsAnOrdLoop_def, IsPartOrder_def

from ordLoopAssum, assms show \( \text{Infimum}(r,B) \in L \) using set_inf_not_empty, inf_is_lb, lsq_members unfolding IsAnOrdLoop_def, IsPartOrder_def

qed

The lifted operation is a binary operation on the powerset of \(L\). This is just a special case of lift_subsets_binop lemma from func_ZF theory.

lemma (in loop1) lifted_op_pow:

shows \( (A \text{ lifted to subsets of } L): Pow(L)\times Pow(L)\rightarrow Pow(L) \) using qgroupassum, lift_subsets_binop unfolding IsAquasigroup_def

Suppose we have two subsets \(B,C\subseteq G\) of the ordered group \(G\) and both of these subsets have infima. Then \((\inf B)\cdot (\inf C)\) is a lower bound of \(B\cdot C = \{x\cdot y: x\in B,y\in C\}\). Unfortunately Isabelle/ZF does not allow the \(\{x+y: x\in B, y\in C\}\) syntax, we have to write \(\{x+y: \langle x,y\rangle\in B\times C\}\) instead.

lemma (in loop1) sum_inf_lower_bound:

assumes \( \text{HasAnInfimum}(r,B) \), \( \text{HasAnInfimum}(r,C) \), \( g\in \{x + y.\ \langle x,y\rangle \in B\times C\} \)

shows \( \text{Infimum}(r,B) + \text{Infimum}(r,C) \leq g \) using ordLoopAssum, assms, inf_is_lb, add_ineq unfolding IsAnOrdLoop_def, IsPartOrder_def

Suppose we have two subsets \(A,B\subseteq G\) of the ordered group \(G\), both of these subsets have infima and also the set \(A\cdot B = \{x\cdot y: x\in A,y\in B\}\) has an infimum. Then \((\inf (A))\cdot (\inf B)\leq \inf (A\cdot B)\). It seems that to show equality one needs the order relation to be linear and the operation to be commutative, so this is done in the context of ordered groups. Please let me know if one can show the equality between \((\inf A) + (\inf B)\) and \(\inf A+B\) in a more general context.

lemma (in loop1) sum_inf_ineq:

assumes \( \text{HasAnInfimum}(r,B) \), \( \text{HasAnInfimum}(r,C) \), \( \text{HasAnInfimum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) \)

shows \( \text{Infimum}(r,B) + \text{Infimum}(r,C) \leq \text{Infimum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) \)proof

let \( D = \{x + y.\ \langle x,y\rangle \in B\times C\} \)

from assms(1,2) have \( \forall g\in D.\ \text{Infimum}(r,B) + \text{Infimum}(r,C) \leq g \) using sum_inf_lower_bound

with ordLoopAssum, assms(3) show \( thesis \) using inf_geq_lo_bnd unfolding IsAnOrdLoop_def, IsPartOrder_def

qed

Shifting a set that has a supremum by a loop element shifts its supremum the same way.

lemma (in loop1) sup_shift:

assumes \( \text{HasAsupremum}(r,B) \), \( x\in L \)

shows \( \text{HasAsupremum}(r,\{x + y.\ y\in B\}) \), \( x + \text{Supremum}(r,B) = \text{Supremum}(r,\{x + y.\ y\in B\}) \), \( \text{HasAsupremum}(r,\{y + x.\ y\in B\}) \), \( \text{Supremum}(r,B) + x = \text{Supremum}(r,\{y + x.\ y\in B\}) \)proof

let \( s = \text{Supremum}(r,B) \)

let \( C = \{x + y.\ y\in B\} \)

let \( D = \{y + x.\ y\in B\} \)

from ordLoopAssum, assms(1) have \( \text{antisym}(r) \), \( r\subseteq L\times L \), \( B\neq \emptyset \), \( C\neq \emptyset \), \( D\neq \emptyset \), \( s\in L \), \( B\subseteq L \) using set_sup_not_empty, sup_in_space, loop_has_sup_subset(1) unfolding IsAnOrdLoop_def, IsPartOrder_def, HasAsupremum_def

from assms, \( \text{antisym}(r) \) have I: \( \forall z\in C.\ \langle z,x + s\rangle \in r \) using sup_is_ub, ord_trans_inv(2)

{

fix \( b \)

assume A: \( \forall z\in C.\ z\leq b \)

with \( C \neq \emptyset \) have \( b\in L \) using lsq_members(2)

from A, \( B\subseteq L \), \( x\in L \) have \( \forall y\in B.\ y \leq - x + b \) using ineq_move_side_left

with assms(1), \( \text{antisym}(r) \), \( x\in L \) have \( x + s \leq x + ( - x + b) \) using sup_leq_up_bnd, ord_trans_inv(2)

with \( x\in L \), \( b\in L \) have \( x + s \leq b \) using lrdiv_props(6)

}

hence II: \( \forall b.\ (\forall z\in C.\ \langle z,b\rangle \in r) \longrightarrow \langle x + s,b\rangle \in r \)

with \( \text{antisym}(r) \), \( C\neq \emptyset \), I show \( \text{HasAsupremum}(r,C) \) using Order_ZF_5_L5(1) unfolding HasAsupremum_def

from \( \text{antisym}(r) \), \( C\neq \emptyset \), I, II show \( x + s = \text{Supremum}(r,C) \) using Order_ZF_5_L5(2)

from assms, \( \text{antisym}(r) \) have III: \( \forall z\in D.\ \langle z,s + x\rangle \in r \) using sup_is_ub, ord_trans_inv(1)

{

fix \( b \)

assume A: \( \forall z\in D.\ z\leq b \)

with \( D \neq \emptyset \) have \( b\in L \) using lsq_members(2)

from A, \( B\subseteq L \), \( x\in L \) have \( \forall y\in B.\ y \leq b - x \) using ineq_move_side_right

with assms(1), \( \text{antisym}(r) \), \( x\in L \) have \( s + x \leq (b - x) + x \) using sup_leq_up_bnd, ord_trans_inv(1)

with \( x\in L \), \( b\in L \) have \( s + x \leq b \) using lrdiv_props(3)

}

hence IV: \( \forall b.\ (\forall z\in D.\ \langle z,b\rangle \in r) \longrightarrow \langle s + x,b\rangle \in r \)

with \( \text{antisym}(r) \), \( D\neq \emptyset \), III show \( \text{HasAsupremum}(r,D) \) using Order_ZF_5_L5(1) unfolding HasAsupremum_def

from \( \text{antisym}(r) \), \( D\neq \emptyset \), III, IV show \( s + x = \text{Supremum}(r,D) \) using Order_ZF_5_L5(2)

qed

Shifting a set that has an infimum by a loop element shifts its infimum the same way.

lemma (in loop1) inf_shift:

assumes \( \text{HasAnInfimum}(r,B) \), \( x\in L \)

shows \( \text{HasAnInfimum}(r,\{x + y.\ y\in B\}) \), \( x + \text{Infimum}(r,B) = \text{Infimum}(r,\{x + y.\ y\in B\}) \), \( \text{HasAnInfimum}(r,\{y + x.\ y\in B\}) \), \( \text{Infimum}(r,B) + x = \text{Infimum}(r,\{y + x.\ y\in B\}) \)proof

let \( m = \text{Infimum}(r,B) \)

let \( C = \{x + y.\ y\in B\} \)

let \( D = \{y + x.\ y\in B\} \)

from ordLoopAssum, assms(1) have \( \text{antisym}(r) \), \( r\subseteq L\times L \), \( B\neq \emptyset \), \( C\neq \emptyset \), \( D\neq \emptyset \), \( m\in L \), \( B\subseteq L \) using set_inf_not_empty, inf_in_space, loop_has_inf_subset(1) unfolding IsAnOrdLoop_def, IsPartOrder_def, HasAnInfimum_def

from assms, \( \text{antisym}(r) \) have I: \( \forall z\in C.\ \langle x + m,z\rangle \in r \) using inf_is_lb, ord_trans_inv(2)

{

fix \( b \)

assume A: \( \forall z\in C.\ b\leq z \)

with \( C \neq \emptyset \) have \( b\in L \) using lsq_members(1)

from A, \( B\subseteq L \), \( x\in L \) have \( \forall y\in B.\ ( - x + b)\leq y \) using ineq_move_side_left1

with assms(1), \( \text{antisym}(r) \), \( x\in L \) have \( x + ( - x + b) \leq x + m \) using inf_geq_lo_bnd, ord_trans_inv(2)

with \( x\in L \), \( b\in L \) have \( b \leq x + m \) using lrdiv_props(6)

}

hence II: \( \forall b.\ (\forall z\in C.\ \langle b,z\rangle \in r) \longrightarrow \langle b,x + m\rangle \in r \)

with \( \text{antisym}(r) \), \( C\neq \emptyset \), I show \( \text{HasAnInfimum}(r,C) \) using inf_glb(1) unfolding HasAnInfimum_def

from \( \text{antisym}(r) \), \( C\neq \emptyset \), I, II show \( x + \text{Infimum}(r,B) = \text{Infimum}(r,C) \) using inf_glb(2)

from assms, \( \text{antisym}(r) \) have III: \( \forall z\in D.\ \langle m + x,z\rangle \in r \) using inf_is_lb, ord_trans_inv(1)

{

fix \( b \)

assume A: \( \forall z\in D.\ b\leq z \)

with \( D \neq \emptyset \) have \( b\in L \) using lsq_members(1)

from A, \( B\subseteq L \), \( x\in L \) have \( \forall y\in B.\ b - x \leq y \) using ineq_move_side_right1

with assms(1), \( \text{antisym}(r) \), \( x\in L \) have \( (b - x) + x \leq m + x \) using inf_geq_lo_bnd, ord_trans_inv(1)

with \( x\in L \), \( b\in L \) have \( b \leq m + x \) using lrdiv_props(3)

}

hence IV: \( \forall b.\ (\forall z\in D.\ \langle b,z\rangle \in r) \longrightarrow \langle b,m + x\rangle \in r \)

with \( \text{antisym}(r) \), \( D\neq \emptyset \), III show \( \text{HasAnInfimum}(r,\{y + x.\ y\in B\}) \) using inf_glb(1) unfolding HasAnInfimum_def

from \( \text{antisym}(r) \), \( D\neq \emptyset \), III, IV show \( m + x = \text{Infimum}(r,D) \) using inf_glb(2)

qed

Suppose sets \(B,C\subseteq L\) have suprema and consider the sets \(S_B = \{\sup (x+C): x\in B\}\) and \(S_C = \{\sup (B+y): y\in C\}\) where \(x+C =\{ x+y:y\in C\}\) and \(B+y = \{x+y:x\in B\}\). Then \(S_B\) and \(S_C\) have suprema equal to \(\sup (B) + \sup (C)\).

lemma (in loop1) sup_sup_exists:

assumes \( \text{HasAsupremum}(r,B) \) and \( \text{HasAsupremum}(r,C) \)

shows \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,\{x + y.\ y\in C\}).\ x\in B\}) \), \( \text{Supremum}(r,\{ \text{Supremum}(r,\{x + y.\ y\in C\}).\ x\in B\}) = \) \( \text{Supremum}(r,B) + \text{Supremum}(r,C) \), \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,\{x + y.\ x\in B\}).\ y\in C\}) \), \( \text{Supremum}(r,\{ \text{Supremum}(r,\{x + y.\ x\in B\}).\ y\in C\}) = \) \( \text{Supremum}(r,B) + \text{Supremum}(r,C) \)proof

let \( s_B = \text{Supremum}(r,B) \)

let \( s_C = \text{Supremum}(r,C) \)

from ordLoopAssum, assms have \( s_B \in L \) and \( s_C \in L \) unfolding IsAnOrdLoop_def, IsPartOrder_def, HasAsupremum_def using sup_in_space

{

fix \( x \)

assume \( x\in B \)

with assms(1) have \( x\in L \) using loop_has_sup_subset(1)

with assms(2) have \( \text{Supremum}(r,\{x + y.\ y\in C\}) = x + s_C \) using sup_shift(2)

}

hence \( \{ \text{Supremum}(r,\{x + y.\ y\in C\}).\ x\in B\} = \{x + s_C.\ x\in B\} \)

with assms(1), \( s_C \in L \) show \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,\{x + y.\ y\in C\}).\ x\in B\}) \) and \( \text{Supremum}(r,\{ \text{Supremum}(r,\{x + y.\ y\in C\}).\ x\in B\}) = s_B + s_C \) using sup_shift(3,4)

{

fix \( y \)

assume \( y\in C \)

with assms(2) have \( y\in L \) using loop_has_sup_subset(1)

with assms(1) have \( \text{Supremum}(r,\{x + y.\ x\in B\}) = s_B + y \) using sup_shift(4)

}

hence \( \{ \text{Supremum}(r,\{x + y.\ x\in B\}).\ y\in C\} = \{s_B + y.\ y\in C\} \)

with assms(2), \( s_B \in L \) show \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,\{x + y.\ x\in B\}).\ y\in C\}) \) and \( \text{Supremum}(r,\{ \text{Supremum}(r,\{x + y.\ x\in B\}).\ y\in C\}) = s_B + s_C \) using sup_shift(1,2)

qed

Suppose sets \(B,C\subseteq L\) have infima and consider the sets \(i_B = \{\inf (x+C): x\in B\}\) and \(i_C = \{\inf (B+y): y\in C\}\) where \(x+C =\{ x+y:y\in C\}\) and \(B+y = \{x+y:x\in B\}\). Then \(i_B\) and \(i_C\) have infima equal to \(\inf (B) + \inf (C)\).

lemma (in loop1) inf_inf_exists:

assumes \( \text{HasAnInfimum}(r,B) \) and \( \text{HasAnInfimum}(r,C) \)

shows \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,\{x + y.\ y\in C\}).\ x\in B\}) \), \( \text{Infimum}(r,\{ \text{Infimum}(r,\{x + y.\ y\in C\}).\ x\in B\}) = \) \( \text{Infimum}(r,B) + \text{Infimum}(r,C) \), \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,\{x + y.\ x\in B\}).\ y\in C\}) \), \( \text{Infimum}(r,\{ \text{Infimum}(r,\{x + y.\ x\in B\}).\ y\in C\}) = \) \( \text{Infimum}(r,B) + \text{Infimum}(r,C) \)proof

let \( i_B = \text{Infimum}(r,B) \)

let \( i_C = \text{Infimum}(r,C) \)

from ordLoopAssum, assms have \( i_B \in L \) and \( i_C \in L \) unfolding IsAnOrdLoop_def, IsPartOrder_def, HasAnInfimum_def using inf_in_space

{

fix \( x \)

assume \( x\in B \)

with assms(1) have \( x\in L \) using loop_has_inf_subset(1)

with assms(2) have \( \text{Infimum}(r,\{x + y.\ y\in C\}) = x + i_C \) using inf_shift(2)

}

hence \( \{ \text{Infimum}(r,\{x + y.\ y\in C\}).\ x\in B\} = \{x + i_C.\ x\in B\} \)

with assms(1), \( i_C \in L \) show \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,\{x + y.\ y\in C\}).\ x\in B\}) \) and \( \text{Infimum}(r,\{ \text{Infimum}(r,\{x + y.\ y\in C\}).\ x\in B\}) = i_B + i_C \) using inf_shift(3,4)

{

fix \( y \)

assume \( y\in C \)

with assms(2) have \( y\in L \) using loop_has_inf_subset(1)

with assms(1) have \( \text{Infimum}(r,\{x + y.\ x\in B\}) = i_B + y \) using inf_shift(4)

}

hence \( \{ \text{Infimum}(r,\{x + y.\ x\in B\}).\ y\in C\} = \{i_B + y.\ y\in C\} \)

with assms(2), \( i_B \in L \) show \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,\{x + y.\ x\in B\}).\ y\in C\}) \) and \( \text{Infimum}(r,\{ \text{Infimum}(r,\{x + y.\ x\in B\}).\ y\in C\}) = i_B + i_C \) using inf_shift(1,2)

qed

If sets \(A,B\subseteq L\) have suprema then the sum of sets (i.e. \(\{x+y:x\in B,y\in C\}\)) also has a supremum equal to the sum of the suprema of \(B\) and \(C\).

theorem (in loop1) ordloop_sup_sum_sum_sup:

assumes \( \text{HasAsupremum}(r,B) \) and \( \text{HasAsupremum}(r,C) \)

shows \( \text{HasAsupremum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) \) and \( \text{Supremum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) = \text{Supremum}(r,B) + \text{Supremum}(r,C) \)proof

let \( \mathcal{T} = \{\{x + y.\ x\in B\}.\ y\in C\} \)

from assms have I: \( \{x + y.\ \langle x,y\rangle \in B\times C\} = \bigcup \mathcal{T} \) and \( B\subseteq L \), \( C\subseteq L \) using cart_prod_union(1), loop_has_sup_subset(1)

from ordLoopAssum have \( r \subseteq L\times L \), \( \text{antisym}(r) \), \( \text{trans}(r) \) unfolding IsAnOrdLoop_def, IsPartOrder_def

moreover

from assms(1), \( C\subseteq L \) have \( \forall T\in \mathcal{T} .\ \text{HasAsupremum}(r,T) \) using sup_shift(3)

moreover

have II: \( \{ \text{Supremum}(r,T).\ T\in \mathcal{T} \} = \{ \text{Supremum}(r,\{x + y.\ x\in B\}).\ y\in C\} \)

with assms have \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) \) using sup_sup_exists(3)

ultimately have \( \text{HasAsupremum}(r,\bigcup \mathcal{T} ) \) and \( \text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) = \text{Supremum}(r,\bigcup \mathcal{T} ) \) using sup_sup

with assms, I, II, \( \text{HasAsupremum}(r,\bigcup \mathcal{T} ) \) show \( \text{HasAsupremum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) \) and \( \text{Supremum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) = \text{Supremum}(r,B) + \text{Supremum}(r,C) \) using sup_sup_exists(4)

qed

If sets \(B,C\subseteq L\) have infima then the Minkowski's sum of sets \(B,C\) (i.e. \(\{x+y:x\in B,y\in C\}\)) also has an infimum equal to the sum of the infima of \(B\) and \(C\).

theorem (in loop1) ordloop_inf_sum_sum_inf:

assumes \( \text{HasAnInfimum}(r,B) \) and \( \text{HasAnInfimum}(r,C) \)

shows \( \text{HasAnInfimum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) \) and \( \text{Infimum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) = \text{Infimum}(r,B) + \text{Infimum}(r,C) \)proof

let \( \mathcal{T} = \{\{x + y.\ x\in B\}.\ y\in C\} \)

from assms have I: \( \{x + y.\ \langle x,y\rangle \in B\times C\} = \bigcup \mathcal{T} \) and \( B\subseteq L \), \( C\subseteq L \) using cart_prod_union(1), loop_has_inf_subset(1)

from ordLoopAssum have \( r \subseteq L\times L \), \( \text{antisym}(r) \), \( \text{trans}(r) \) unfolding IsAnOrdLoop_def, IsPartOrder_def

moreover

from assms(1), \( C\subseteq L \) have \( \forall T\in \mathcal{T} .\ \text{HasAnInfimum}(r,T) \) using inf_shift(3)

moreover

have II: \( \{ \text{Infimum}(r,T).\ T\in \mathcal{T} \} = \{ \text{Infimum}(r,\{x + y.\ x\in B\}).\ y\in C\} \)

with assms have \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) \) using inf_inf_exists(3)

ultimately have \( \text{HasAnInfimum}(r,\bigcup \mathcal{T} ) \) and \( \text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) = \text{Infimum}(r,\bigcup \mathcal{T} ) \) using inf_inf

with assms, I, II, \( \text{HasAnInfimum}(r,\bigcup \mathcal{T} ) \) show \( \text{HasAnInfimum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) \) and \( \text{Infimum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) = \text{Infimum}(r,B) + \text{Infimum}(r,C) \) using inf_inf_exists(4)

qed

end

lemma loop_loop0_valid:

assumes \( \text{IsAloop}(G,A) \)

shows \( loop0(G,A) \)

Definition of IsAnOrdLoop: \( \text{IsAnOrdLoop}(L,A,r) \equiv \) \( \text{IsAloop}(L,A) \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \forall z\in L.\ \) \( ((\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ))) \)

lemma lrdiv_binop:

assumes \( \text{IsAquasigroup}(G,A) \)

shows \( \text{ LeftDiv}(G,A):G\times G\rightarrow G \) and \( \text{ RightDiv}(G,A):G\times G\rightarrow G \)

lemma (in loop1) lsq_members:

assumes \( x\leq y \)

shows \( x\in L \) and \( y\in L \)

lemma (in loop1) ord_trans_inv:

assumes \( x\leq y \), \( z\in L \)

shows \( x + z \leq y + z \) and \( z + x \leq z + y \)

lemma (in loop1) less_members:

assumes \( x \lt y \)

shows \( x\in L \) and \( y\in L \)

lemma (in quasigroup0) qg_cancel_right:

assumes \( x\in G \), \( y\in G \), \( z\in G \) and \( y\cdot x = z\cdot x \)

shows \( y=z \)

lemma (in quasigroup0) qg_cancel_left:

assumes \( x\in G \), \( y\in G \), \( z\in G \) and \( x\cdot y = x\cdot z \)

shows \( y=z \)

lemma (in group3) ineq_cancel_right:

assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\cdot b \leq c\cdot b \)

shows \( a\leq c \)

lemma (in loop1) ineq_cancel_left:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \leq z + y \)

shows \( x\leq y \)

lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)

shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \)

lemma (in loop1) strict_ineq_cancel_left:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \lt z + y \)

shows \( x \lt y \)

lemma (in loop1) strict_ineq_cancel_right:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( x + z \lt y + z \)

shows \( x \lt y \)

lemma (in loop1) strict_ineq_subtr:

assumes \( x \lt y \), \( z\in L \)

shows \( x - z \lt y - z \) and \( ( - z + x) \lt - z + y \)

lemma (in quasigroup0) lrdiv_ident:

assumes \( x\in G \), \( y\in G \)

shows \( (y\cdot x)/ x = y \) and \( x\backslash (x\cdot y) = y \)

lemma (in loop1) ineq_subtr_from_sides:

assumes \( x\leq y \), \( z\in L \)

shows \( x - z \leq y - z \) and \( ( - z + x) \leq - z + y \)

lemma (in loop1) ineq_subtr_from_sides:

assumes \( x\leq y \), \( z\in L \)

shows \( x - z \leq y - z \) and \( ( - z + x) \leq - z + y \)

lemma (in quasigroup0) lrdiv_ident:

assumes \( x\in G \), \( y\in G \)

shows \( (y\cdot x)/ x = y \) and \( x\backslash (x\cdot y) = y \)

Definition of Nonnegative: \( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)

Definition of PositiveSet: \( \text{PositiveSet}(L,A,r) \equiv \) \( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} \)

Definition of IsPartOrder: \( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)

lemma Fol1_L4:

assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)

shows \( a=b \)

lemma Fol1_L3:

assumes \( \text{trans}(r) \) and \( \langle a,b\rangle \in r \wedge \langle b,c\rangle \in r \)

shows \( \langle a,c\rangle \in r \)

lemma (in loop0) neut_props_loop: shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)

lemma (in loop1) loop_ord_refl:

assumes \( x\in L \)

shows \( x\leq x \)

lemma (in loop1) nonneg_definition: shows \( x \in L^+ \longleftrightarrow 0 \leq x \)

lemma (in loop1) loop_ord_trans:

assumes \( x\leq y \) and \( y\leq z \)

shows \( x\leq z \)

lemma (in loop1) loop_ord_antisym:

assumes \( x\leq y \) and \( y\leq x \)

shows \( x=y \)

lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)

lemma (in loop0) neut_props_loop: shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)

lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)

lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)

lemma (in loop1) posset_definition1: shows \( x \in L_+ \longleftrightarrow 0 \lt x \)

lemma (in loop1) lsq_members:

assumes \( x\leq y \)

shows \( x\in L \) and \( y\in L \)

lemma (in loop1) ord_trans_inv:

assumes \( x\leq y \), \( z\in L \)

shows \( x + z \leq y + z \) and \( z + x \leq z + y \)

lemma (in loop1) lsq_members:

assumes \( x\leq y \)

shows \( x\in L \) and \( y\in L \)

lemma (in loop1) ord_trans_inv:

assumes \( x\leq y \), \( z\in L \)

shows \( x + z \leq y + z \) and \( z + x \leq z + y \)

lemma (in loop1) less_members:

assumes \( x \lt y \)

shows \( x\in L \) and \( y\in L \)

lemma (in loop1) strict_ord_trans_inv:

assumes \( x \lt y \), \( z\in L \)

shows \( x + z \lt y + z \) and \( z + x \lt z + y \)

lemma (in loop1) less_members:

assumes \( x \lt y \)

shows \( x\in L \) and \( y\in L \)

lemma (in loop1) strict_ord_trans_inv:

assumes \( x \lt y \), \( z\in L \)

shows \( x + z \lt y + z \) and \( z + x \lt z + y \)

lemma (in loop1) loop_strict_ord_trans2:

assumes \( x \lt y \) and \( y \lt z \)

shows \( x \lt z \)

lemma (in loop1) loop_strict_ord_trans:

assumes \( x\leq y \) and \( y \lt z \)

shows \( x \lt z \)

lemma (in loop1) loop_strict_ord_trans1:

assumes \( x \lt y \) and \( y\leq z \)

shows \( x \lt z \)

lemma (in loop1) add_ineq_strict1:

assumes \( x\leq y \), \( z \lt t \)

shows \( x + z \lt y + t \) and \( z + x \lt t + y \)

lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)

lemma (in loop1) add_ineq_strict1:

assumes \( x\leq y \), \( z \lt t \)

shows \( x + z \lt y + t \) and \( z + x \lt t + y \)

lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)

lemma (in loop1) add_ineq:

assumes \( x\leq y \), \( z\leq t \)

shows \( x + z \leq y + t \)

lemma (in loop0) neut_props_loop: shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)

Definition of IsOpClosed: \( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)

lemma (in loop1) nonneg_subset: shows \( L^+ \subseteq L \)

lemma (in loop1) loop_zero_nonneg: shows \( 0 \in L^+ \)

lemma (in loop1) nonneg_closed: shows \( L^+ \text{ is closed under } A \)

lemma fold_in_op_closed:

assumes \( n\in nat \), \( f:X\times X\rightarrow X \), \( s:n\rightarrow A \), \( A\subseteq X \), \( x\in A \) and \( A \text{ is closed under } f \)

shows \( \text{Fold}(f,x,s) \in A \)

Definition of IsAloop: \( \text{IsAloop}(G,A) \equiv \text{IsAquasigroup}(G,A) \wedge (\exists e\in G.\ \forall x\in G.\ A\langle e,x\rangle = x \wedge A\langle x,e\rangle = x) \)

Definition of IsAquasigroup: \( \text{IsAquasigroup}(G,A) \equiv A:G\times G\rightarrow G \wedge A \text{ has Latin square property on } G \)

lemma (in loop1) positive_subset: shows \( L_+ \subseteq L \)

lemma down_directs_subset:

assumes \( r \text{ down-directs } A \), \( \text{IsPartOrder}(X,r) \), \( A\subseteq X \)

shows \( \text{IsDownDirectedSet}(A,r) \)

Definition of IsBoundedBelow: \( \text{IsBoundedBelow}(A,r) \equiv \exists l.\ \forall x\in A.\ \langle l,x\rangle \in r \)

lemma inf_geq_lo_bnd:

assumes \( \text{antisym}(r) \), \( \text{HasAnInfimum}(r,A) \), \( \forall a\in A.\ \langle u,a\rangle \in r \)

shows \( \langle u, \text{Infimum}(r,A)\rangle \in r \)

lemma Order_ZF_4_L15:

assumes \( \text{antisym}(r) \) and \( m\in A \) and \( \forall a\in A.\ \langle m,a\rangle \in r \)

shows \( \text{HasAminimum}(r,A) \) and \( \text{Minimum}(r,A) = m \)

lemma min_is_inf:

assumes \( \text{antisym}(r) \), \( \text{HasAminimum}(r,A) \)

shows \( \text{HasAnInfimum}(r,A) \) and \( \text{Minimum}(r,A) = \text{Infimum}(r,A) \)

lemma (in loop0) loop_pow_mult_one:

assumes \( n\in nat \), \( x\in G \)

shows \( x^{n + 1} = x^{n}\cdot x \)

corollary (in loop0) loop_zero_pow: shows \( x^{0} = 1 \)

lemma (in loop0) loop_prod_type:

assumes \( n\in nat \), \( x\in G \)

shows \( x^{n} \in G \)

lemma (in loop1) add_subtract_pos:

assumes \( x\in L \), \( 0 \lt y \)

shows \( x - y \lt x \), \( ( - y + x) \lt x \), \( x \lt x + y \), \( x \lt y + x \)

lemma ind_on_nat1:

assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(k + 1) \)

shows \( P(n) \)

lemma nat_not0_succ:

assumes \( n\in nat \), \( n\neq 0 \)

shows \( \exists m\in nat.\ n = m + 1 \)

corollary (in loop0) loop_not_empty: shows \( G\neq \emptyset \)

lemma compl_bounded_sup_props:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( r \text{ is complete } \) and \( A\neq 0 \), \( \text{IsBoundedAbove}(A,r) \)

shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \)

lemma compl_bounded_sup_props:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( r \text{ is complete } \) and \( A\neq 0 \), \( \text{IsBoundedAbove}(A,r) \)

shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \)

lemma (in loop1) ineq_move_side_right:

assumes \( x\in L \), \( y\in L \), \( x + y\leq z \)

shows \( x\leq z - y \)

lemma compl_sup_leq_up_bnd:

assumes \( \text{antisym}(r) \), \( r \text{ is complete } \), \( A\neq \emptyset \), \( \forall a\in A.\ \langle a,u\rangle \in r \)

shows \( \langle \text{Supremum}(r,A),u\rangle \in r \)

lemma (in loop1) add_subtract_pos:

assumes \( x\in L \), \( 0 \lt y \)

shows \( x - y \lt x \), \( ( - y + x) \lt x \), \( x \lt x + y \), \( x \lt y + x \)

lemma (in loop1) nat_mult_not_bounded:

assumes \( r \text{ is complete } \) and \( 0 \lt x \)

shows \( \neg \text{IsBoundedAbove}(\{n\cdot x.\ n\in nat\setminus \{0\}\},r) \)

Definition of IsBoundedAbove: \( \text{IsBoundedAbove}(A,r) \equiv \exists u.\ \forall x\in A.\ \langle x,u\rangle \in r \)

lemma (in loop1) mults_pos_pos:

assumes \( 0 \lt x \), \( n\in nat\setminus \{0\} \)

shows \( 0 \lt n\cdot x \)

lemma (in loop1) posset_definition: shows \( x \in L_+ \longleftrightarrow ( 0 \leq x \wedge x\neq 0 ) \)

Definition of IsTotal: \( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)

Definition of IsArchimedean: \( B \text{ is Archimedean } \equiv B\neq \emptyset \wedge (\forall x\in B.\ \forall y\in B.\ \exists n\in nat\setminus \{0\}.\ y \lt n\cdot x) \)

lemma has_sup_subset:

assumes \( r\subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAsupremum}(r,A) \)

shows \( A\subseteq X \)

lemma set_sup_not_empty:

assumes \( \text{HasAsupremum}(r,A) \)

shows \( A\neq \emptyset \)

lemma sup_is_ub:

assumes \( \text{antisym}(r) \), \( \text{HasAsupremum}(r,A) \), \( x\in A \)

shows \( \langle x, \text{Supremum}(r,A)\rangle \in r \)

lemma has_inf_subset:

assumes \( r\subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAnInfimum}(r,A) \)

shows \( A\subseteq X \)

lemma set_inf_not_empty:

assumes \( \text{HasAnInfimum}(r,A) \)

shows \( A\neq \emptyset \)

lemma inf_is_lb:

assumes \( \text{antisym}(r) \), \( \text{HasAnInfimum}(r,A) \), \( x\in A \)

shows \( \langle \text{Infimum}(r,A),x\rangle \in r \)

lemma lift_subsets_binop:

assumes \( f : X \times X \rightarrow Y \)

shows \( (f \text{ lifted to subsets of } X) : Pow(X) \times Pow(X) \rightarrow Pow(Y) \)

lemma (in loop1) sum_inf_lower_bound:

assumes \( \text{HasAnInfimum}(r,B) \), \( \text{HasAnInfimum}(r,C) \), \( g\in \{x + y.\ \langle x,y\rangle \in B\times C\} \)

shows \( \text{Infimum}(r,B) + \text{Infimum}(r,C) \leq g \)

lemma sup_in_space:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)

shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \)

lemma (in loop1) loop_has_sup_subset:

assumes \( \text{HasAsupremum}(r,B) \)

shows \( B\subseteq L \) and \( \text{Supremum}(r,B) \in L \)

Definition of HasAsupremum: \( \text{HasAsupremum}(r,A) \equiv \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)

lemma (in loop1) ineq_move_side_left:

assumes \( x\in L \), \( y\in L \), \( x + y\leq z \)

shows \( y \leq - x + z \)

lemma sup_leq_up_bnd:

assumes \( \text{antisym}(r) \), \( \text{HasAsupremum}(r,A) \), \( \forall a\in A.\ \langle a,u\rangle \in r \)

shows \( \langle \text{Supremum}(r,A),u\rangle \in r \)

lemma Order_ZF_5_L5:

assumes \( \text{antisym}(r) \) and \( A\neq 0 \) and \( \forall x\in A.\ \langle x,z\rangle \in r \) and \( \forall y.\ (\forall x\in A.\ \langle x,y\rangle \in r) \longrightarrow \langle z,y\rangle \in r \)

shows \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \), \( z = \text{Supremum}(r,A) \)

lemma Order_ZF_5_L5:

shows \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \), \( z = \text{Supremum}(r,A) \)

lemma inf_in_space:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)

shows \( \text{Infimum}(r,A) \in X \) and \( \forall x\in A.\ \langle \text{Infimum}(r,A),x\rangle \in r \)

lemma (in loop1) loop_has_inf_subset:

assumes \( \text{HasAnInfimum}(r,B) \)

shows \( B\subseteq L \) and \( \text{Infimum}(r,B) \in L \)

Definition of HasAnInfimum: \( \text{HasAnInfimum}(r,A) \equiv \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)

lemma (in loop1) ineq_move_side_left1:

assumes \( x\in L \), \( y\in L \), \( z\leq x + y \)

shows \( ( - x + z) \leq y \)

lemma inf_glb:

assumes \( \text{antisym}(r) \), \( A\neq \emptyset \), \( \forall x\in A.\ \langle z,x\rangle \in r \), \( \forall y.\ (\forall x\in A.\ \langle y,x\rangle \in r) \longrightarrow \langle y,z\rangle \in r \)

shows \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \) and \( z = \text{Infimum}(r,A) \)

lemma inf_glb:

shows \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \) and \( z = \text{Infimum}(r,A) \)

lemma (in loop1) ineq_move_side_right1:

assumes \( x\in L \), \( y\in L \), \( z\leq x + y \)

shows \( z - y\leq x \)

lemma (in loop1) sup_shift:

assumes \( \text{HasAsupremum}(r,B) \), \( x\in L \)

lemma (in loop1) sup_shift:

assumes \( \text{HasAsupremum}(r,B) \), \( x\in L \)

lemma (in loop1) sup_shift:

assumes \( \text{HasAsupremum}(r,B) \), \( x\in L \)

lemma (in loop1) sup_shift:

assumes \( \text{HasAsupremum}(r,B) \), \( x\in L \)

lemma (in loop1) inf_shift:

assumes \( \text{HasAnInfimum}(r,B) \), \( x\in L \)

lemma (in loop1) inf_shift:

assumes \( \text{HasAnInfimum}(r,B) \), \( x\in L \)

lemma (in loop1) inf_shift:

assumes \( \text{HasAnInfimum}(r,B) \), \( x\in L \)

lemma (in loop1) inf_shift:

assumes \( \text{HasAnInfimum}(r,B) \), \( x\in L \)

lemma cart_prod_union: shows \( \{b(x,y).\ \langle x,y\rangle \in X\times Y\} = \bigcup \{\{b(x,y).\ x\in X\} .\ y\in Y\} \), \( \{b(x,y).\ \langle x,y\rangle \in X\times Y\} = \bigcup \{\{b(x,y).\ y\in Y\} .\ x\in X\} \)

lemma (in loop1) sup_shift:

assumes \( \text{HasAsupremum}(r,B) \), \( x\in L \)

lemma (in loop1) sup_sup_exists:

assumes \( \text{HasAsupremum}(r,B) \) and \( \text{HasAsupremum}(r,C) \)

lemma sup_sup:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{trans}(r) \), \( \forall T\in \mathcal{T} .\ \text{HasAsupremum}(r,T) \), \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) \)

shows \( \text{HasAsupremum}(r,\bigcup \mathcal{T} ) \) and \( \text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) = \text{Supremum}(r,\bigcup \mathcal{T} ) \)

lemma (in loop1) sup_sup_exists:

assumes \( \text{HasAsupremum}(r,B) \) and \( \text{HasAsupremum}(r,C) \)

lemma (in loop1) inf_shift:

assumes \( \text{HasAnInfimum}(r,B) \), \( x\in L \)

lemma (in loop1) inf_inf_exists:

assumes \( \text{HasAnInfimum}(r,B) \) and \( \text{HasAnInfimum}(r,C) \)

lemma inf_inf:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{trans}(r) \), \( \forall T\in \mathcal{T} .\ \text{HasAnInfimum}(r,T) \), \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) \)

shows \( \text{HasAnInfimum}(r,\bigcup \mathcal{T} ) \) and \( \text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) = \text{Infimum}(r,\bigcup \mathcal{T} ) \)

lemma (in loop1) inf_inf_exists:

assumes \( \text{HasAnInfimum}(r,B) \) and \( \text{HasAnInfimum}(r,C) \)