theory OrderedGroup_ZF_1 imports OrderedGroup_ZF
begin
In this theory we continue the OrderedGroup_ZF theory development.
Absolute value and the triangle inequality
The goal of this section is to prove the triangle inequality for ordered groups.
Absolute value maps \(G\) into \(G\).
lemma (in group3) OrderedGroup_ZF_3_L1:
shows \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G \)proof let \( f = id(G^+) \)
let \( g = \text{restrict}( \text{GroupInv}(G,P),G-G^+) \)
have \( f : G^+\rightarrow G^+ \) using id_type
then have \( f : G^+\rightarrow G \) using OrderedGroup_ZF_1_L4E, fun_weaken_type
moreover
have \( g : G-G^+\rightarrow G \)proof
moreover from ordGroupAssum have \( \text{GroupInv}(G,P) : G\rightarrow G \) using IsAnOrdGroup_def, group0_2_T2
moreover
qed
have \( G-G^+ \subseteq G \)
ultimately show \( thesis \) using restrict_type2
have \( G^+\cap (G-G^+) = 0 \)
ultimately have \( f \cup g : G^+\cup (G-G^+)\rightarrow G\cup G \) by (rule fun_disjoint_Un )
moreover
qed
have \( G^+\cup (G-G^+) = G \) using OrderedGroup_ZF_1_L4E
ultimately show \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G \) using AbsoluteValue_def
If \(a\in G^+\), then \(|a| = a\).
lemma (in group3) OrderedGroup_ZF_3_L2:
assumes A1: \( a\in G^+ \)
shows \( \vert a\vert = a \)proof from ordGroupAssum have \( \text{GroupInv}(G,P) : G\rightarrow G \) using IsAnOrdGroup_def, group0_2_T2
with A1 show \( thesis \) using func1_1_L1, OrderedGroup_ZF_1_L4E, fun_disjoint_apply1, AbsoluteValue_def, id_conv
qed
The absolute value of the unit is the unit. In the additive totation that would be \(|0| = 0\).
lemma (in group3) OrderedGroup_ZF_3_L2A:
shows \( \vert 1 \vert = 1 \) using OrderedGroup_ZF_1_L3A, OrderedGroup_ZF_3_L2If \(a\) is positive, then \(|a| = a\).
lemma (in group3) OrderedGroup_ZF_3_L2B:
assumes \( a\in G_+ \)
shows \( \vert a\vert = a \) using assms, PositiveSet_def, Nonnegative_def, OrderedGroup_ZF_3_L2If \(a\in G\setminus G^+\), then \(|a| = a^{-1}\).
lemma (in group3) OrderedGroup_ZF_3_L3:
assumes A1: \( a \in G-G^+ \)
shows \( \vert a\vert = a^{-1} \)proof have \( domain(id(G^+)) = G^+ \) using id_type, func1_1_L1
with A1 show \( thesis \) using fun_disjoint_apply2, AbsoluteValue_def, restrict
qed
For elements that not greater than the unit, the absolute value is the inverse.
lemma (in group3) OrderedGroup_ZF_3_L3A:
assumes A1: \( a\leq 1 \)
shows \( \vert a\vert = a^{-1} \)proof{
}
assume \( a=1 \)
then have \( \vert a\vert = a^{-1} \) using OrderedGroup_ZF_3_L2A, OrderedGroup_ZF_1_L1, group_inv_of_one
moreover {
}
ultimately show \( \vert a\vert = a^{-1} \)
qed
assume \( a\neq 1 \)
with A1 have \( \vert a\vert = a^{-1} \) using OrderedGroup_ZF_1_L4C, OrderedGroup_ZF_3_L3
In linearly ordered groups the absolute value of any element is in \(G^+\).
lemma (in group3) OrderedGroup_ZF_3_L3B:
assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \)
shows \( \vert a\vert \in G^+ \)proof{
}
assume \( a \in G^+ \)
then have \( \vert a\vert \in G^+ \) using OrderedGroup_ZF_3_L2
moreover {
}
ultimately show \( \vert a\vert \in G^+ \)
qed
assume \( a \notin G^+ \)
with A1, A2 have \( \vert a\vert \in G^+ \) using OrderedGroup_ZF_3_L3, OrderedGroup_ZF_1_L6
For linearly ordered groups (where the order is total), the absolute value maps the group into the positive set.
lemma (in group3) OrderedGroup_ZF_3_L3C:
assumes A1: \( r \text{ is total on } G \)
shows \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G^+ \)proof have \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G \) using OrderedGroup_ZF_3_L1
moreover
qed
from A1 have T2: \( \forall g\in G.\ \text{AbsoluteValue}(G,P,r)(g) \in G^+ \) using OrderedGroup_ZF_3_L3B
ultimately show \( thesis \) by (rule func1_1_L1A )
If the absolute value is the unit, then the elemnent is the unit.
lemma (in group3) OrderedGroup_ZF_3_L3D:
assumes A1: \( a\in G \) and A2: \( \vert a\vert = 1 \)
shows \( a = 1 \)proof{
}
assume \( a \in G^+ \)
with A2 have \( a = 1 \) using OrderedGroup_ZF_3_L2
moreover {
}
ultimately show \( a = 1 \)
qed
assume \( a \notin G^+ \)
with A1, A2 have \( a = 1 \) using OrderedGroup_ZF_3_L3, OrderedGroup_ZF_1_L1, group0_2_L8A
In linearly ordered groups the unit is not greater than the absolute value of any element.
lemma (in group3) OrderedGroup_ZF_3_L3E:
assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( 1 \leq \vert a\vert \) using assms, OrderedGroup_ZF_3_L3B, OrderedGroup_ZF_1_L2If \(b\) is greater than both \(a\) and \(a^{-1}\), then \(b\) is greater than \(|a|\).
lemma (in group3) OrderedGroup_ZF_3_L4:
assumes A1: \( a\leq b \) and A2: \( a^{-1}\leq b \)
shows \( \vert a\vert \leq b \)proof{
}
assume \( a\in G^+ \)
with A1 have \( \vert a\vert \leq b \) using OrderedGroup_ZF_3_L2
moreover {
}
ultimately show \( \vert a\vert \leq b \)
qed
assume \( a\notin G^+ \)
with A1, A2 have \( \vert a\vert \leq b \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_3_L3
In linearly ordered groups \(a\leq |a|\).
lemma (in group3) OrderedGroup_ZF_3_L5:
assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \)
shows \( a \leq \vert a\vert \)proof{
}
assume \( a \in G^+ \)
with A2 have \( a \leq \vert a\vert \) using OrderedGroup_ZF_3_L2, OrderedGroup_ZF_1_L3
moreover {
}
ultimately show \( a \leq \vert a\vert \)
qed
assume \( a \notin G^+ \)
with A1, A2 have \( a \leq \vert a\vert \) using OrderedGroup_ZF_3_L3B, OrderedGroup_ZF_1_L4B
\(a^{-1}\leq |a|\) (in additive notation it would be \(-a\leq |a|\).
lemma (in group3) OrderedGroup_ZF_3_L6:
assumes A1: \( a\in G \)
shows \( a^{-1} \leq \vert a\vert \)proof{
}
assume \( a \in G^+ \)
then have T1: \( 1 \leq a \) and T2: \( \vert a\vert = a \) using OrderedGroup_ZF_1_L2, OrderedGroup_ZF_3_L2
then have \( a^{-1}\leq 1 ^{-1} \) using OrderedGroup_ZF_1_L5
then have T3: \( a^{-1}\leq 1 \) using OrderedGroup_ZF_1_L1, group_inv_of_one
from T3, T1 have \( a^{-1}\leq a \) by (rule Group_order_transitive )
with T2 have \( a^{-1} \leq \vert a\vert \)
moreover {
}
ultimately show \( a^{-1} \leq \vert a\vert \)
qed
assume A2: \( a \notin G^+ \)
from A1 have \( \vert a\vert \in G \) using OrderedGroup_ZF_3_L1, apply_funtype
with ordGroupAssum have \( \vert a\vert \leq \vert a\vert \) using IsAnOrdGroup_def, IsPartOrder_def, refl_def
with A1, A2 have \( a^{-1} \leq \vert a\vert \) using OrderedGroup_ZF_3_L3
Some inequalities about the product of two elements of a linearly ordered group and its absolute value.
lemma (in group3) OrderedGroup_ZF_3_L6A:
assumes \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \)
shows \( a\cdot b \leq \vert a\vert \cdot \vert b\vert \), \( a\cdot b^{-1} \leq \vert a\vert \cdot \vert b\vert \), \( a^{-1}\cdot b \leq \vert a\vert \cdot \vert b\vert \), \( a^{-1}\cdot b^{-1} \leq \vert a\vert \cdot \vert b\vert \) using assms, OrderedGroup_ZF_3_L5, OrderedGroup_ZF_3_L6, OrderedGroup_ZF_1_L5B\(|a^{-1}|\leq |a|\).
lemma (in group3) OrderedGroup_ZF_3_L7:
assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( \vert a^{-1}\vert \leq \vert a\vert \) using assms, OrderedGroup_ZF_3_L5, OrderedGroup_ZF_1_L1, group_inv_of_inv, OrderedGroup_ZF_3_L6, OrderedGroup_ZF_3_L4\(|a^{-1}| = |a|\).
lemma (in group3) OrderedGroup_ZF_3_L7A:
assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \)
shows \( \vert a^{-1}\vert = \vert a\vert \)proof from A2 have \( a^{-1}\in G \) using OrderedGroup_ZF_1_L1, inverse_in_group
with A1 have \( \vert (a^{-1})^{-1}\vert \leq \vert a^{-1}\vert \) using OrderedGroup_ZF_3_L7
with A1, A2 have \( \vert a^{-1}\vert \leq \vert a\vert \), \( \vert a\vert \leq \vert a^{-1}\vert \) using OrderedGroup_ZF_1_L1, group_inv_of_inv, OrderedGroup_ZF_3_L7
then show \( thesis \) by (rule group_order_antisym )
qed
\(|a\cdot b^{-1}| = |b\cdot a^{-1}|\). It doesn't look so strange in the additive notation: \(|a-b| = |b-a|\).
lemma (in group3) OrderedGroup_ZF_3_L7B:
assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \), \( b\in G \)
shows \( \vert a\cdot b^{-1}\vert = \vert b\cdot a^{-1}\vert \)proof from A1, A2 have \( \vert (a\cdot b^{-1})^{-1}\vert = \vert a\cdot b^{-1}\vert \) using OrderedGroup_ZF_1_L1, inverse_in_group, group0_2_L1, group0_1_L1, OrderedGroup_ZF_3_L7A
moreover
qed
from A2 have \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \) using OrderedGroup_ZF_1_L1, group0_2_L12
ultimately show \( thesis \)
Triangle inequality for linearly ordered abelian groups. It would be nice to drop commutativity or give an example that shows we can't do that.
theorem (in group3) OrdGroup_triangle_ineq:
assumes A1: \( P \text{ is commutative on } G \) and A2: \( r \text{ is total on } G \) and A3: \( a\in G \), \( b\in G \)
shows \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \)proof from A1, A2, A3 have \( a \leq \vert a\vert \), \( b \leq \vert b\vert \), \( a^{-1} \leq \vert a\vert \), \( b^{-1} \leq \vert b\vert \) using OrderedGroup_ZF_3_L5, OrderedGroup_ZF_3_L6
then have \( a\cdot b \leq \vert a\vert \cdot \vert b\vert \), \( a^{-1}\cdot b^{-1} \leq \vert a\vert \cdot \vert b\vert \) using OrderedGroup_ZF_1_L5B
with A1, A3 show \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \) using OrderedGroup_ZF_1_L1, group_inv_of_two, IsCommutative_def, OrderedGroup_ZF_3_L4
qed
We can multiply the sides of an inequality with absolute value.
lemma (in group3) OrderedGroup_ZF_3_L7C:
assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \), \( a\in G \), \( b\in G \) and \( \vert a\vert \leq c \), \( \vert b\vert \leq d \)
shows \( \vert a\cdot b\vert \leq c\cdot d \)proof from assms(1,2,3,4) have \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \) using OrdGroup_triangle_ineq
moreover
qed
from assms(5,6) have \( \vert a\vert \cdot \vert b\vert \leq c\cdot d \) using OrderedGroup_ZF_1_L5B
ultimately show \( thesis \) by (rule Group_order_transitive )
A version of the OrderedGroup_ZF_3_L7C but with multiplying by the inverse.
lemma (in group3) OrderedGroup_ZF_3_L7CA:
assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \vert a\vert \leq c \), \( \vert b\vert \leq d \)
shows \( \vert a\cdot b^{-1}\vert \leq c\cdot d \) using assms, OrderedGroup_ZF_1_L1, inverse_in_group, OrderedGroup_ZF_3_L7A, OrderedGroup_ZF_3_L7CTriangle inequality with three integers.
lemma (in group3) OrdGroup_triangle_ineq3:
assumes A1: \( P \text{ is commutative on } G \) and A2: \( r \text{ is total on } G \) and A3: \( a\in G \), \( b\in G \), \( c\in G \)
shows \( \vert a\cdot b\cdot c\vert \leq \vert a\vert \cdot \vert b\vert \cdot \vert c\vert \)proof from A3 have T: \( a\cdot b \in G \), \( \vert c\vert \in G \) using OrderedGroup_ZF_1_L1, group_op_closed, OrderedGroup_ZF_3_L1, apply_funtype
with A1, A2, A3 have \( \vert a\cdot b\cdot c\vert \leq \vert a\cdot b\vert \cdot \vert c\vert \) using OrdGroup_triangle_ineq
moreover
qed
from ordGroupAssum, A1, A2, A3, T have \( \vert a\cdot b\vert \cdot \vert c\vert \leq \vert a\vert \cdot \vert b\vert \cdot \vert c\vert \) using OrdGroup_triangle_ineq, IsAnOrdGroup_def
ultimately show \( \vert a\cdot b\cdot c\vert \leq \vert a\vert \cdot \vert b\vert \cdot \vert c\vert \) by (rule Group_order_transitive )
Some variants of the triangle inequality.
lemma (in group3) OrderedGroup_ZF_3_L7D:
assumes A1: \( P \text{ is commutative on } G \) and A2: \( r \text{ is total on } G \) and A3: \( a\in G \), \( b\in G \) and A4: \( \vert a\cdot b^{-1}\vert \leq c \)
shows \( \vert a\vert \leq c\cdot \vert b\vert \), \( \vert a\vert \leq \vert b\vert \cdot c \), \( c^{-1}\cdot a \leq b \), \( a\cdot c^{-1} \leq b \), \( a \leq b\cdot c \)proof from A3, A4 have T: \( a\cdot b^{-1} \in G \), \( \vert b\vert \in G \), \( c\in G \), \( c^{-1} \in G \) using OrderedGroup_ZF_1_L1, inverse_in_group, group0_2_L1, group0_1_L1, OrderedGroup_ZF_3_L1, apply_funtype, OrderedGroup_ZF_1_L4
from A3 have \( \vert a\vert = \vert a\cdot b^{-1}\cdot b\vert \) using OrderedGroup_ZF_1_L1, inv_cancel_two
with A1, A2, A3, T have \( \vert a\vert \leq \vert a\cdot b^{-1}\vert \cdot \vert b\vert \) using OrdGroup_triangle_ineq
with T, A4 show \( \vert a\vert \leq c\cdot \vert b\vert \) using OrderedGroup_ZF_1_L5C
with T, A1 show \( \vert a\vert \leq \vert b\vert \cdot c \) using IsCommutative_def
from A2, T have \( a\cdot b^{-1} \leq \vert a\cdot b^{-1}\vert \) using OrderedGroup_ZF_3_L5
moreover
note A4
ultimately have I: \( a\cdot b^{-1} \leq c \) by (rule Group_order_transitive )
with A3 show \( c^{-1}\cdot a \leq b \) using OrderedGroup_ZF_1_L5H
with A1, A3, T show \( a\cdot c^{-1} \leq b \) using IsCommutative_def
from A1, A3, T, I show \( a \leq b\cdot c \) using OrderedGroup_ZF_1_L5H, IsCommutative_def
qed
Some more variants of the triangle inequality.
lemma (in group3) OrderedGroup_ZF_3_L7E:
assumes A1: \( P \text{ is commutative on } G \) and A2: \( r \text{ is total on } G \) and A3: \( a\in G \), \( b\in G \) and A4: \( \vert a\cdot b^{-1}\vert \leq c \)
shows \( b\cdot c^{-1} \leq a \)proof from A3 have \( a\cdot b^{-1} \in G \) using OrderedGroup_ZF_1_L1, inverse_in_group, group_op_closed
with A2 have \( \vert (a\cdot b^{-1})^{-1}\vert = \vert a\cdot b^{-1}\vert \) using OrderedGroup_ZF_3_L7A
moreover
qed
from A3 have \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \) using OrderedGroup_ZF_1_L1, group0_2_L12
ultimately have \( \vert b\cdot a^{-1}\vert = \vert a\cdot b^{-1}\vert \)
with A1, A2, A3, A4 show \( b\cdot c^{-1} \leq a \) using OrderedGroup_ZF_3_L7D
An application of the triangle inequality with four group elements.
lemma (in group3) OrderedGroup_ZF_3_L7F:
assumes A1: \( P \text{ is commutative on } G \) and A2: \( r \text{ is total on } G \) and A3: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)
shows \( \vert a\cdot c^{-1}\vert \leq \vert a\cdot b\vert \cdot \vert c\cdot d\vert \cdot \vert b\cdot d^{-1}\vert \)proof from A3 have T: \( a\cdot c^{-1} \in G \), \( a\cdot b \in G \), \( c\cdot d \in G \), \( b\cdot d^{-1} \in G \), \( (c\cdot d)^{-1} \in G \), \( (b\cdot d^{-1})^{-1} \in G \) using OrderedGroup_ZF_1_L1, inverse_in_group, group_op_closed
with A1, A2 have \( \vert (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1}\vert \leq \vert a\cdot b\vert \cdot \vert (c\cdot d)^{-1}\vert \cdot \vert (b\cdot d^{-1})^{-1}\vert \) using OrdGroup_triangle_ineq3
moreover
qed
from A2, T have \( \vert (c\cdot d)^{-1}\vert =\vert c\cdot d\vert \) and \( \vert (b\cdot d^{-1})^{-1}\vert = \vert b\cdot d^{-1}\vert \) using OrderedGroup_ZF_3_L7A
moreover from A1, A3 have \( (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1} \) using OrderedGroup_ZF_1_L1, group0_4_L8
ultimately show \( \vert a\cdot c^{-1}\vert \leq \vert a\cdot b\vert \cdot \vert c\cdot d\vert \cdot \vert b\cdot d^{-1}\vert \)
\(|a|\leq L\) implies \(L^{-1} \leq a\) (it would be \(-L \leq a\) in the additive notation).
lemma (in group3) OrderedGroup_ZF_3_L8:
assumes A1: \( a\in G \) and A2: \( \vert a\vert \leq L \)
shows \( L^{-1}\leq a \)proof from A1 have I: \( a^{-1} \leq \vert a\vert \) using OrderedGroup_ZF_3_L6
from I, A2 have \( a^{-1} \leq L \) by (rule Group_order_transitive )
then have \( L^{-1}\leq (a^{-1})^{-1} \) using OrderedGroup_ZF_1_L5
with A1 show \( L^{-1}\leq a \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
qed
In linearly ordered groups \(|a|\leq L\) implies \(a \leq L\) (it would be \(a \leq L\) in the additive notation).
lemma (in group3) OrderedGroup_ZF_3_L8A:
assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \) and A3: \( \vert a\vert \leq L \)
shows \( a\leq L \), \( 1 \leq L \)proof from A1, A2 have I: \( a \leq \vert a\vert \) using OrderedGroup_ZF_3_L5
from I, A3 show \( a\leq L \) by (rule Group_order_transitive )
from A1, A2, A3 have \( 1 \leq \vert a\vert \), \( \vert a\vert \leq L \) using OrderedGroup_ZF_3_L3B, OrderedGroup_ZF_1_L2
then show \( 1 \leq L \) by (rule Group_order_transitive )
qed
A somewhat generalized version of the above lemma.
lemma (in group3) OrderedGroup_ZF_3_L8B:
assumes A1: \( a\in G \) and A2: \( \vert a\vert \leq L \) and A3: \( 1 \leq c \)
shows \( (L\cdot c)^{-1} \leq a \)proof from A1, A2, A3 have \( c^{-1}\cdot L^{-1} \leq 1 \cdot a \) using OrderedGroup_ZF_3_L8, OrderedGroup_ZF_1_L5AB, OrderedGroup_ZF_1_L5B
with A1, A2, A3 show \( (L\cdot c)^{-1} \leq a \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L1, group_inv_of_two, group0_2_L2
qed
If \(b\) is between \(a\) and \(a\cdot c\), then \(b\cdot a^{-1}\leq c\).
lemma (in group3) OrderedGroup_ZF_3_L8C:
assumes A1: \( a\leq b \) and A2: \( c\in G \) and A3: \( b\leq c\cdot a \)
shows \( \vert b\cdot a^{-1}\vert \leq c \)proof from A1, A2, A3 have \( b\cdot a^{-1} \leq c \) using OrderedGroup_ZF_1_L9C, OrderedGroup_ZF_1_L4
moreover
qed
have \( (b\cdot a^{-1})^{-1} \leq c \)proof
ultimately show \( \vert b\cdot a^{-1}\vert \leq c \) using OrderedGroup_ZF_3_L4
from A1 have T: \( a\in G \), \( b\in G \) using OrderedGroup_ZF_1_L4
with A1 have \( a\cdot b^{-1} \leq 1 \) using OrderedGroup_ZF_1_L9
moreover
qed
from A1, A3 have \( a\leq c\cdot a \) by (rule Group_order_transitive )
with ordGroupAssum, T have \( a\cdot a^{-1} \leq c\cdot a\cdot a^{-1} \) using OrderedGroup_ZF_1_L1, inverse_in_group, IsAnOrdGroup_def
with T, A2 have \( 1 \leq c \) using OrderedGroup_ZF_1_L1, group0_2_L6, inv_cancel_two
ultimately have \( a\cdot b^{-1} \leq c \) by (rule Group_order_transitive )
with T show \( (b\cdot a^{-1})^{-1} \leq c \) using OrderedGroup_ZF_1_L1, group0_2_L12
For linearly ordered groups if the absolute values of elements in a set are bounded, then the set is bounded.
lemma (in group3) OrderedGroup_ZF_3_L9:
assumes A1: \( r \text{ is total on } G \) and A2: \( A\subseteq G \) and A3: \( \forall a\in A.\ \vert a\vert \leq L \)
shows \( \text{IsBounded}(A,r) \)proof from A1, A2, A3 have \( \forall a\in A.\ a\leq L \), \( \forall a\in A.\ L^{-1}\leq a \) using OrderedGroup_ZF_3_L8, OrderedGroup_ZF_3_L8A
then show \( \text{IsBounded}(A,r) \) using IsBoundedAbove_def, IsBoundedBelow_def, IsBounded_def
qed
A slightly more general version of the previous lemma, stating the same fact for a set defined by separation.
lemma (in group3) OrderedGroup_ZF_3_L9A:
assumes A1: \( r \text{ is total on } G \) and A2: \( \forall x\in X.\ b(x)\in G \wedge \vert b(x)\vert \leq L \)
shows \( \text{IsBounded}(\{b(x).\ x\in X\},r) \)proof from A2 have \( \{b(x).\ x\in X\} \subseteq G \), \( \forall a\in \{b(x).\ x\in X\}.\ \vert a\vert \leq L \)
with A1 show \( thesis \) using OrderedGroup_ZF_3_L9
qed
A special form of the previous lemma stating a similar fact for an image of a set by a function with values in a linearly ordered group.
lemma (in group3) OrderedGroup_ZF_3_L9B:
assumes A1: \( r \text{ is total on } G \) and A2: \( f:X\rightarrow G \) and A3: \( A\subseteq X \) and A4: \( \forall x\in A.\ \vert f(x)\vert \leq L \)
shows \( \text{IsBounded}(f(A),r) \)proof from A2, A3, A4 have \( \forall x\in A.\ f(x) \in G \wedge \vert f(x)\vert \leq L \) using apply_funtype
with A1 have \( \text{IsBounded}(\{f(x).\ x\in A\},r) \) by (rule OrderedGroup_ZF_3_L9A )
with A2, A3 show \( \text{IsBounded}(f(A),r) \) using func_imagedef
qed
For linearly ordered groups if \(l\leq a\leq u\) then \(|a|\) is smaller than the greater of \(|l|,|u|\).
lemma (in group3) OrderedGroup_ZF_3_L10:
assumes A1: \( r \text{ is total on } G \) and A2: \( l\leq a \), \( a\leq u \)
shows \( \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \)proof from A2 have T1: \( \vert l\vert \in G \), \( \vert a\vert \in G \), \( \vert u\vert \in G \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_3_L1, apply_funtype
{
assume A3: \( a\in G^+ \)
with A2 have \( 1 \leq a \), \( a\leq u \) using OrderedGroup_ZF_1_L2
then have \( 1 \leq u \) by (rule Group_order_transitive )
with A2, A3 have \( \vert a\vert \leq \vert u\vert \) using OrderedGroup_ZF_1_L2, OrderedGroup_ZF_3_L2
moreover
from A1, T1 have \( \vert u\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) using Order_ZF_3_L2
ultimately have \( \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) by (rule Group_order_transitive )
moreover {
}
ultimately show \( thesis \)
qed
assume A4: \( a\notin G^+ \)
with A2 have T2: \( l\in G \), \( \vert l\vert \in G \), \( \vert a\vert \in G \), \( \vert u\vert \in G \), \( a \in G-G^+ \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_3_L1, apply_funtype
with A2 have \( l \in G-G^+ \) using OrderedGroup_ZF_1_L4D
with T2, A2 have \( \vert a\vert \leq \vert l\vert \) using OrderedGroup_ZF_3_L3, OrderedGroup_ZF_1_L5
moreover
from A1, T2 have \( \vert l\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) using Order_ZF_3_L2
ultimately have \( \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) by (rule Group_order_transitive )
For linearly ordered groups if a set is bounded then the absolute values are bounded.
lemma (in group3) OrderedGroup_ZF_3_L10A:
assumes A1: \( r \text{ is total on } G \) and A2: \( \text{IsBounded}(A,r) \)
shows \( \exists L.\ \forall a\in A.\ \vert a\vert \leq L \)proof{
}
assume \( A = 0 \)
then have \( thesis \)
moreover {
}
ultimately show \( thesis \)
qed
assume A3: \( A\neq 0 \)
with A2 have \( \exists u.\ \forall g\in A.\ g\leq u \) and \( \exists l.\ \forall g\in A.\ l\leq g \) using IsBounded_def, IsBoundedAbove_def, IsBoundedBelow_def
then obtain \( u \) \( l \) where \( \forall g\in A.\ l\leq g \wedge g\leq u \)
with A1 have \( \forall a\in A.\ \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) using OrderedGroup_ZF_3_L10
then have \( thesis \)
A slightly more general version of the previous lemma, stating the same fact for a set defined by separation.
lemma (in group3) OrderedGroup_ZF_3_L11:
assumes \( r \text{ is total on } G \) and \( \text{IsBounded}(\{b(x).\ x\in X\},r) \)
shows \( \exists L.\ \forall x\in X.\ \vert b(x)\vert \leq L \) using assms, OrderedGroup_ZF_3_L10AAbsolute values of elements of a finite image of a nonempty set are bounded by an element of the group.
lemma (in group3) OrderedGroup_ZF_3_L11A:
assumes A1: \( r \text{ is total on } G \) and A2: \( X\neq 0 \) and A3: \( \{b(x).\ x\in X\} \in Fin(G) \)
shows \( \exists L\in G.\ \forall x\in X.\ \vert b(x)\vert \leq L \)proof from A1, A3 have \( \exists L.\ \forall x\in X.\ \vert b(x)\vert \leq L \) using ord_group_fin_bounded, OrderedGroup_ZF_3_L11
then obtain \( L \) where I: \( \forall x\in X.\ \vert b(x)\vert \leq L \) using OrderedGroup_ZF_3_L11
from A2 obtain \( x \) where \( x\in X \)
with I show \( thesis \) using OrderedGroup_ZF_1_L4
qed
In totally ordered groups the absolute value of a nonunit element is in \( G_+ \).
lemma (in group3) OrderedGroup_ZF_3_L12:
assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \) and A3: \( a\neq 1 \)
shows \( \vert a\vert \in G_+ \)proof from A1, A2 have \( \vert a\vert \in G \), \( 1 \leq \vert a\vert \) using OrderedGroup_ZF_3_L1, apply_funtype, OrderedGroup_ZF_3_L3B, OrderedGroup_ZF_1_L2
moreover
qed
from A2, A3 have \( \vert a\vert \neq 1 \) using OrderedGroup_ZF_3_L3D
ultimately show \( \vert a\vert \in G_+ \) using PositiveSet_def
Maximum absolute value of a set
Quite often when considering inequalities we prefer to talk about the absolute values instead of raw elements of a set. This section formalizes some material that is useful for that.
If a set has a maximum and minimum, then the greater of the absolute value of the maximum and minimum belongs to the image of the set by the absolute value function.
lemma (in group3) OrderedGroup_ZF_4_L1:
assumes \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( M = \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)
shows \( M \in \text{AbsoluteValue}(G,P,r)(A) \) using ordGroupAssum, assms, IsAnOrdGroup_def, IsPartOrder_def, Order_ZF_4_L3, Order_ZF_4_L4, OrderedGroup_ZF_3_L1, func_imagedef, GreaterOf_defIf a set has a maximum and minimum, then the greater of the absolute value of the maximum and minimum bounds absolute values of all elements of the set.
lemma (in group3) OrderedGroup_ZF_4_L2:
assumes A1: \( r \text{ is total on } G \) and A2: \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and A3: \( a\in A \)
shows \( \vert a\vert \leq \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)proof from ordGroupAssum, A2, A3 have \( \text{Minimum}(r,A)\leq a \), \( a\leq \text{Maximum}(r,A) \) using IsAnOrdGroup_def, IsPartOrder_def, Order_ZF_4_L3, Order_ZF_4_L4
with A1 show \( thesis \) by (rule OrderedGroup_ZF_3_L10 )
qed
If a set has a maximum and minimum, then the greater of the absolute value of the maximum and minimum bounds absolute values of all elements of the set. In this lemma the absolute values of ekements of a set are represented as the elements of the image of the set by the absolute value function.
lemma (in group3) OrderedGroup_ZF_4_L3:
assumes \( r \text{ is total on } G \) and \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( b \in \text{AbsoluteValue}(G,P,r)(A) \)
shows \( b\leq \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \) using assms, OrderedGroup_ZF_3_L1, func_imagedef, OrderedGroup_ZF_4_L2If a set has a maximum and minimum, then the set of absolute values also has a maximum.
lemma (in group3) OrderedGroup_ZF_4_L4:
assumes A1: \( r \text{ is total on } G \) and A2: \( A \subseteq G \) and A3: \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \)
shows \( \text{HasAmaximum}(r, \text{AbsoluteValue}(G,P,r)(A)) \)proof let \( M = \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)
from A2, A3 have \( M \in \text{AbsoluteValue}(G,P,r)(A) \) using OrderedGroup_ZF_4_L1
moreover
qed
from A1, A2, A3 have \( \forall b \in \text{AbsoluteValue}(G,P,r)(A).\ b \leq M \) using OrderedGroup_ZF_4_L3
ultimately show \( thesis \) using HasAmaximum_def
If a set has a maximum and a minimum, then all absolute values are bounded by the maximum of the set of absolute values.
lemma (in group3) OrderedGroup_ZF_4_L5:
assumes A1: \( r \text{ is total on } G \) and A2: \( A \subseteq G \) and A3: \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and A4: \( a\in A \)
shows \( \vert a\vert \leq \text{Maximum}(r, \text{AbsoluteValue}(G,P,r)(A)) \)proof from A2, A4 have \( \vert a\vert \in \text{AbsoluteValue}(G,P,r)(A) \) using OrderedGroup_ZF_3_L1, func_imagedef
with ordGroupAssum, A1, A2, A3 show \( thesis \) using IsAnOrdGroup_def, IsPartOrder_def, OrderedGroup_ZF_4_L4, Order_ZF_4_L3
qed
Alternative definitions
Sometimes it is usful to define the order by prescibing the set of positive or nonnegative elements. This section deals with two such definitions. One takes a subset \(H\) of \(G\) that is closed under the group operation, \(1\notin H\) and for every \(a\in H\) we have either \(a\in H\) or \(a^{-1}\in H\). Then the order is defined as \(a\leq b\) iff \(a=b\) or \(a^{-1}b \in H\). For abelian groups this makes a linearly ordered group. We will refer to order defined this way in the comments as the order defined by a positive set. The context used in this section is the group0 context defined in Group_ZF theory. Recall that f in that context denotes the group operation (unlike in the previous sections where the group operation was denoted P.
The order defined by a positive set is the same as the order defined by a nonnegative set.
lemma (in group0) OrderedGroup_ZF_5_L1:
assumes A1: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)
shows \( \langle a,b\rangle \in r \longleftrightarrow a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \)proof assume \( \langle a,b\rangle \in r \)
with A1 show \( a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \) using group0_2_L6
next
assume \( a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \)
then have \( a\in G \wedge b\in G \wedge b=(a^{-1})^{-1} \vee a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \) using inverse_in_group, group0_2_L9
with A1 show \( \langle a,b\rangle \in r \) using group_inv_of_inv
qed
The relation defined by a positive set is antisymmetric.
lemma (in group0) OrderedGroup_ZF_5_L2:
assumes A1: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and A2: \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \)
shows \( \text{antisym}(r) \)proof{
}
}
fix \( a \) \( b \)
assume A3: \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)
with A1 have T: \( a\in G \), \( b\in G \)
{
assume A4: \( a\neq b \)
with A1, A3 have \( a^{-1}\cdot b \in G \), \( a^{-1}\cdot b \in H \), \( (a^{-1}\cdot b)^{-1} \in H \) using inverse_in_group, group0_2_L1, group0_1_L1, group0_2_L12
with A2 have \( a^{-1}\cdot b = 1 \) using Xor_def
with T, A4 have \( False \) using group0_2_L11
then have \( a=b \)
then show \( \text{antisym}(r) \) by (rule antisymI )
qed
The relation defined by a positive set is transitive.
lemma (in group0) OrderedGroup_ZF_5_L3:
assumes A1: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and A2: \( H\subseteq G \), \( H \text{ is closed under } P \)
shows \( \text{trans}(r) \)proof{
}
fix \( a \) \( b \) \( c \)
assume \( \langle a,b\rangle \in r \), \( \langle b,c\rangle \in r \)
with A1 have \( a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \), \( b\in G \wedge c\in G \wedge b^{-1}\cdot c \in H \cup \{1 \} \) using OrderedGroup_ZF_5_L1
with A2 have I: \( a\in G \), \( b\in G \), \( c\in G \) and \( (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \in H \cup \{1 \} \) using inverse_in_group, group0_2_L17, IsOpClosed_def
moreover
from I have \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \) by (rule group0_2_L14A )
ultimately have \( \langle a,c\rangle \in G\times G \), \( a^{-1}\cdot c \in H \cup \{1 \} \)
with A1 have \( \langle a,c\rangle \in r \) using OrderedGroup_ZF_5_L1
then have \( \forall a b c.\ \langle a, b\rangle \in r \wedge \langle b, c\rangle \in r \longrightarrow \langle a, c\rangle \in r \)
then show \( \text{trans}(r) \) by (rule Fol1_L2 )
qed
The relation defined by a positive set is translation invariant. With our definition this step requires the group to be abelian.
lemma (in group0) OrderedGroup_ZF_5_L4:
assumes A1: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and A2: \( P \text{ is commutative on } G \) and A3: \( \langle a,b\rangle \in r \) and A4: \( c\in G \)
shows \( \langle a\cdot c,b\cdot c\rangle \in r \wedge \langle c\cdot a,c\cdot b\rangle \in r \)proof from A1, A3, A4 have I: \( a\in G \), \( b\in G \), \( a\cdot c \in G \), \( b\cdot c \in G \) and II: \( a^{-1}\cdot b \in H \cup \{1 \} \) using OrderedGroup_ZF_5_L1, group_op_closed
with A2, A4 have \( (a\cdot c)^{-1}\cdot (b\cdot c) \in H \cup \{1 \} \) using group0_4_L6D
with A1, I show \( \langle a\cdot c,b\cdot c\rangle \in r \) using OrderedGroup_ZF_5_L1
with A2, A4, I show \( \langle c\cdot a,c\cdot b\rangle \in r \) using IsCommutative_def
qed
If \(H\subseteq G\) is closed under the group operation \(1\notin H\) and for every \(a\in H\) we have either \(a\in H\) or \(a^{-1}\in H\), then the relation "\(\leq\)" defined by \(a\leq b \Leftrightarrow a^{-1}b \in H\) orders the group \(G\). In such order \(H\) may be the set of positive or nonnegative elements.
lemma (in group0) OrderedGroup_ZF_5_L5:
assumes A1: \( P \text{ is commutative on } G \) and A2: \( H\subseteq G \), \( H \text{ is closed under } P \) and A3: \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \) and A4: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)
shows \( \text{IsAnOrdGroup}(G,P,r) \), \( r \text{ is total on } G \), \( \text{Nonnegative}(G,P,r) = \text{PositiveSet}(G,P,r) \cup \{1 \} \)proof from groupAssum, A2, A3, A4 have \( \text{IsAgroup}(G,P) \), \( r \subseteq G\times G \), \( \text{IsPartOrder}(G,r) \) using refl_def, OrderedGroup_ZF_5_L2, OrderedGroup_ZF_5_L3, IsPartOrder_def
moreover
{
from A1, A4 have \( \forall g\in G.\ \forall a b.\ \langle a,b\rangle \in r \longrightarrow \langle a\cdot g,b\cdot g\rangle \in r \wedge \langle g\cdot a,g\cdot b\rangle \in r \) using OrderedGroup_ZF_5_L4
ultimately show \( \text{IsAnOrdGroup}(G,P,r) \) using IsAnOrdGroup_def
then show \( \text{Nonnegative}(G,P,r) = \text{PositiveSet}(G,P,r) \cup \{1 \} \) using group3_def, OrderedGroup_ZF_1_L24
fix \( a \) \( b \)
assume T: \( a\in G \), \( b\in G \)
then have T1: \( a^{-1}\cdot b \in G \) using inverse_in_group, group_op_closed
{
assume \( \langle a,b\rangle \notin r \)
with A4, T have I: \( a\neq b \) and II: \( a^{-1}\cdot b \notin H \)
from A3, T, T1, I have \( (a^{-1}\cdot b \in H) \text{ Xor } ((a^{-1}\cdot b)^{-1} \in H) \) using group0_2_L11
with A4, T, II have \( \langle b,a\rangle \in r \) using Xor_def, group0_2_L12
then have \( \langle a,b\rangle \in r \vee \langle b,a\rangle \in r \)
then show \( r \text{ is total on } G \) using IsTotal_def
qed
If the set defined as in OrderedGroup_ZF_5_L4 does not contain the neutral element, then it is the positive set for the resulting order.
lemma (in group0) OrderedGroup_ZF_5_L6:
assumes \( P \text{ is commutative on } G \) and \( H\subseteq G \) and \( 1 \notin H \) and \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)
shows \( \text{PositiveSet}(G,P,r) = H \) using assms, group_inv_of_one, group0_2_L2, PositiveSet_defThe next definition describes how we construct an order relation from the prescribed set of positive elements.
definition
\( \text{OrderFromPosSet}(G,P,H) \equiv \) \( \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee P\langle \text{GroupInv}(G,P)(\text{fst}(p)),\text{snd}(p)\rangle \in H \} \)
The next theorem rephrases lemmas OrderedGroup_ZF_5_L5 and OrderedGroup_ZF_5_L6 using the definition of the order from the positive set OrderFromPosSet. To summarize, this is what it says: Suppose that \(H\subseteq G\) is a set closed under that group operation such that \(1\notin H\) and for every nonunit group element \(a\) either \(a\in H\) or \(a^{-1}\in H\). Define the order as \(a\leq b\) iff \(a=b\) or \(a^{-1}\cdot b \in H\). Then this order makes \(G\) into a linearly ordered group such \(H\) is the set of positive elements (and then of course \(H \cup \{1\}\) is the set of nonnegative elements).
theorem (in group0) Group_ord_by_positive_set:
assumes \( P \text{ is commutative on } G \) and \( H\subseteq G \), \( H \text{ is closed under } P \), \( 1 \notin H \) and \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \)
shows \( \text{IsAnOrdGroup}(G,P, \text{OrderFromPosSet}(G,P,H)) \), \( \text{OrderFromPosSet}(G,P,H) \text{ is total on } G \), \( \text{PositiveSet}(G,P, \text{OrderFromPosSet}(G,P,H)) = H \), \( \text{Nonnegative}(G,P, \text{OrderFromPosSet}(G,P,H)) = H \cup \{1 \} \) using assms, OrderFromPosSet_def, OrderedGroup_ZF_5_L5, OrderedGroup_ZF_5_L6Odd Extensions
In this section we verify properties of odd extensions of functions defined on \(G_+\). An odd extension of a function \(f: G_+ \rightarrow G\) is a function \(f^\circ : G\rightarrow G\) defined by \(f^\circ (x) = f(x)\) if \(x\in G_+\), \(f(1) = 1\) and \(f^\circ (x) = (f(x^{-1}))^{-1}\) for \(x < 1\). Such function is the unique odd function that is equal to \(f\) when restricted to \(G_+\).
The next lemma is just to see the definition of the odd extension in the notation used in the group1 context.
lemma (in group3) OrderedGroup_ZF_6_L1:
shows \( f^\circ = f \cup \{\langle a, (f(a^{-1}))^{-1}\rangle .\ a \in -G_+\} \cup \{\langle 1 ,1 \rangle \} \) using OddExtension_defA technical lemma that states that from a function defined on \( G_+ \) with values in \(G\) we have \((f(a^{-1}))^{-1}\in G\).
lemma (in group3) OrderedGroup_ZF_6_L2:
assumes \( f: G_+\rightarrow G \) and \( a\in -G_+ \)
shows \( f(a^{-1}) \in G \), \( (f(a^{-1}))^{-1} \in G \) using assms, OrderedGroup_ZF_1_L27, apply_funtype, OrderedGroup_ZF_1_L1, inverse_in_groupThe main theorem about odd extensions. It basically says that the odd extension of a function is what we want to to be.
lemma (in group3) odd_ext_props:
assumes A1: \( r \text{ is total on } G \) and A2: \( f: G_+\rightarrow G \)
shows \( f^\circ : G \rightarrow G \), \( \forall a\in G_+.\ (f^\circ )(a) = f(a) \), \( \forall a\in (-G_+).\ (f^\circ )(a) = (f(a^{-1}))^{-1} \), \( (f^\circ )(1 ) = 1 \)proof from A1, A2 have I: \( f: G_+\rightarrow G \), \( \forall a\in -G_+.\ (f(a^{-1}))^{-1} \in G \), \( G_+\cap (-G_+) = 0 \), \( 1 \notin G_+\cup (-G_+) \), \( f^\circ = f \cup \{\langle a, (f(a^{-1}))^{-1}\rangle .\ a \in -G_+\} \cup \{\langle 1 ,1 \rangle \} \) using OrderedGroup_ZF_6_L2, OrdGroup_decomp2, OrderedGroup_ZF_6_L1
then have \( f^\circ : G_+ \cup (-G_+) \cup \{1 \} \rightarrow G\cup G\cup \{1 \} \) by (rule func1_1_L11E )
moreover
from A1 have \( G_+ \cup (-G_+) \cup \{1 \} = G \), \( G\cup G\cup \{1 \} = G \) using OrdGroup_decomp2, OrderedGroup_ZF_1_L1, group0_2_L2
ultimately show \( f^\circ : G \rightarrow G \)
from I show \( \forall a\in G_+.\ (f^\circ )(a) = f(a) \) by (rule func1_1_L11E )
from I show \( \forall a\in (-G_+).\ (f^\circ )(a) = (f(a^{-1}))^{-1} \) by (rule func1_1_L11E )
from I show \( (f^\circ )(1 ) = 1 \) by (rule func1_1_L11E )
qed
Odd extensions are odd, of course.
lemma (in group3) oddext_is_odd:
assumes A1: \( r \text{ is total on } G \) and A2: \( f: G_+\rightarrow G \) and A3: \( a\in G \)
shows \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \)proof from A1, A3 have \( a\in G_+ \vee a \in (-G_+) \vee a=1 \) using OrdGroup_decomp2
moreover {
}
moreover {
}
moreover {
}
ultimately show \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \)
qed
assume \( a\in G_+ \)
with A1, A2 have \( a^{-1} \in -G_+ \) and \( (f^\circ )(a) = f(a) \) using OrderedGroup_ZF_1_L25, odd_ext_props
with A1, A2 have \( (f^\circ )(a^{-1}) = (f((a^{-1})^{-1}))^{-1} \) and \( (f(a))^{-1} = ((f^\circ )(a))^{-1} \) using odd_ext_props
with A3 have \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
assume A4: \( a \in -G_+ \)
with A1, A2 have \( a^{-1} \in G_+ \) and \( (f^\circ )(a) = (f(a^{-1}))^{-1} \) using OrderedGroup_ZF_1_L27, odd_ext_props
with A1, A2, A4 have \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \) using odd_ext_props, OrderedGroup_ZF_6_L2, OrderedGroup_ZF_1_L1, group_inv_of_inv
assume \( a = 1 \)
with A1, A2 have \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \) using OrderedGroup_ZF_1_L1, group_inv_of_one, odd_ext_props
Another way of saying that odd extensions are odd.
lemma (in group3) oddext_is_odd_alt:
assumes A1: \( r \text{ is total on } G \) and A2: \( f: G_+\rightarrow G \) and A3: \( a\in G \)
shows \( ((f^\circ )(a^{-1}))^{-1} = (f^\circ )(a) \)proof from A1, A2 have \( f^\circ : G \rightarrow G \), \( \forall a\in G.\ (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \) using odd_ext_props, oddext_is_odd
then have \( \forall a\in G.\ ((f^\circ )(a^{-1}))^{-1} = (f^\circ )(a) \) using OrderedGroup_ZF_1_L1, group0_6_L2
with A3 show \( ((f^\circ )(a^{-1}))^{-1} = (f^\circ )(a) \)
qed
Functions with infinite limits
In this section we consider functions \(f: G\rightarrow G\) with the property that for \(f(x)\) is arbitrarily large for large enough \(x\). More precisely, for every \(a\in G\) there exist \(b\in G_+\) such that for every \(x\geq b\) we have \(f(x)\geq a\). In a sense this means that \(\lim_{x\rightarrow \infty}f(x) = \infty\), hence the title of this section. We also prove dual statements for functions such that \(\lim_{x\rightarrow -\infty}f(x) = -\infty\).
If an image of a set by a function with infinite positive limit is bounded above, then the set itself is bounded above.
lemma (in group3) OrderedGroup_ZF_7_L1:
assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( f:G\rightarrow G \) and A4: \( \forall a\in G.\ \exists b\in G_+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) and A5: \( A\subseteq G \) and A6: \( \text{IsBoundedAbove}(f(A),r) \)
shows \( \text{IsBoundedAbove}(A,r) \)proof{
}
assume \( \neg \text{IsBoundedAbove}(A,r) \)
then have I: \( \forall u.\ \exists x\in A.\ \neg (x\leq u) \) using IsBoundedAbove_def
have \( \forall a\in G.\ \exists y\in f(A).\ a\leq y \)proof
{
}
fix \( a \)
assume \( a\in G \)
with A4 obtain \( b \) where II: \( b\in G_+ \) and III: \( \forall x.\ b\leq x \longrightarrow a \leq f(x) \)
from I obtain \( x \) where IV: \( x\in A \) and \( \neg (x\leq b) \)
with A1, A5, II have \( r \text{ is total on } G \), \( x\in G \), \( b\in G \), \( \neg (x\leq b) \) using PositiveSet_def
with III have \( a \leq f(x) \) using OrderedGroup_ZF_1_L8
with A3, A5, IV have \( \exists y\in f(A).\ a\leq y \) using func_imagedef
thus \( thesis \)
qed
with A1, A2, A6 have \( False \) using OrderedGroup_ZF_2_L2A
thus \( thesis \)
qed
If an image of a set defined by separation by a function with infinite positive limit is bounded above, then the set itself is bounded above.
lemma (in group3) OrderedGroup_ZF_7_L2:
assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( X\neq 0 \) and A4: \( f:G\rightarrow G \) and A5: \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq f(y) \) and A6: \( \forall x\in X.\ b(x) \in G \wedge f(b(x)) \leq U \)
shows \( \exists u.\ \forall x\in X.\ b(x) \leq u \)proof let \( A = \{b(x).\ x\in X\} \)
from A6 have I: \( A\subseteq G \)
moreover
qed
note assms
moreover have \( \text{IsBoundedAbove}(f(A),r) \)proof
ultimately have \( \text{IsBoundedAbove}(A,r) \) using OrderedGroup_ZF_7_L1
from A4, A6, I have \( \forall z\in f(A).\ \langle z,U\rangle \in r \) using func_imagedef
then show \( \text{IsBoundedAbove}(f(A),r) \) by (rule Order_ZF_3_L10 )
qed
with A3 have \( \exists u.\ \forall y\in A.\ y \leq u \) using IsBoundedAbove_def
then show \( \exists u.\ \forall x\in X.\ b(x) \leq u \)
If the image of a set defined by separation by a function with infinite negative limit is bounded below, then the set itself is bounded above. This is dual to OrderedGroup_ZF_7_L2.
lemma (in group3) OrderedGroup_ZF_7_L3:
assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( X\neq 0 \) and A4: \( f:G\rightarrow G \) and A5: \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a \) and A6: \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \)
shows \( \exists l.\ \forall x\in X.\ l \leq b(x) \)proof let \( g = \text{GroupInv}(G,P)\circ f\circ \text{GroupInv}(G,P) \)
from ordGroupAssum have I: \( \text{GroupInv}(G,P) : G\rightarrow G \) using IsAnOrdGroup_def, group0_2_T2
with A4 have II: \( \forall x\in G.\ g(x) = (f(x^{-1}))^{-1} \) using func1_1_L18
note A1, A2, A3
moreover
qed
from A4, I have \( g : G\rightarrow G \) using comp_fun
moreover have \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq g(y) \)proof
moreover {
}
fix \( a \)
assume A7: \( a\in G \)
then have \( a^{-1} \in G \) using OrderedGroup_ZF_1_L1, inverse_in_group
with A5 obtain \( b \) where III: \( b\in G_+ \) and \( \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a^{-1} \)
with II, A7 have \( \forall y.\ b\leq y \longrightarrow a \leq g(y) \) using OrderedGroup_ZF_1_L5AD, OrderedGroup_ZF_1_L4
with III have \( \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq g(y) \)
then show \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq g(y) \)
qed
have \( \forall x\in X.\ b(x)^{-1} \in G \wedge g(b(x)^{-1}) \leq L^{-1} \)proof
ultimately have \( \exists u.\ \forall x\in X.\ (b(x))^{-1} \leq u \) by (rule OrderedGroup_ZF_7_L2 )
{
}
fix \( x \)
assume \( x\in X \)
with A6 have T: \( b(x) \in G \), \( b(x)^{-1} \in G \) and \( L \leq f(b(x)) \) using OrderedGroup_ZF_1_L1, inverse_in_group
then have \( (f(b(x)))^{-1} \leq L^{-1} \) using OrderedGroup_ZF_1_L5
moreover
from II, T have \( (f(b(x)))^{-1} = g(b(x)^{-1}) \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
ultimately have \( g(b(x)^{-1}) \leq L^{-1} \)
with T have \( b(x)^{-1} \in G \wedge g(b(x)^{-1}) \leq L^{-1} \)
then show \( \forall x\in X.\ b(x)^{-1} \in G \wedge g(b(x)^{-1}) \leq L^{-1} \)
qed
then have \( \exists u.\ \forall x\in X.\ u^{-1} \leq (b(x)^{-1})^{-1} \) using OrderedGroup_ZF_1_L5
with A6 show \( \exists l.\ \forall x\in X.\ l \leq b(x) \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
The next lemma combines OrderedGroup_ZF_7_L2 and OrderedGroup_ZF_7_L3 to show that if an image of a set defined by separation by a function with infinite limits is bounded, then the set itself i bounded.
lemma (in group3) OrderedGroup_ZF_7_L4:
assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( X\neq 0 \) and A4: \( f:G\rightarrow G \) and A5: \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq f(y) \) and A6: \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a \) and A7: \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \wedge f(b(x)) \leq U \)
shows \( \exists M.\ \forall x\in X.\ \vert b(x)\vert \leq M \)proof from A7 have I: \( \forall x\in X.\ b(x) \in G \wedge f(b(x)) \leq U \) and II: \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \)
from A1, A2, A3, A4, A5, I have \( \exists u.\ \forall x\in X.\ b(x) \leq u \) by (rule OrderedGroup_ZF_7_L2 )
moreover
qed
from A1, A2, A3, A4, A6, II have \( \exists l.\ \forall x\in X.\ l \leq b(x) \) by (rule OrderedGroup_ZF_7_L3 )
ultimately have \( \exists u l.\ \forall x\in X.\ l\leq b(x) \wedge b(x) \leq u \)
with A1 have \( \exists u l.\ \forall x\in X.\ \vert b(x)\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) using OrderedGroup_ZF_3_L10
then show \( \exists M.\ \forall x\in X.\ \vert b(x)\vert \leq M \)
end
lemma (in group3) OrderedGroup_ZF_1_L4E: shows \( G^+ \subseteq G \)
Definition of IsAnOrdGroup:
\( \text{IsAnOrdGroup}(G,P,r) \equiv \)
\( ( \text{IsAgroup}(G,P) \wedge r\subseteq G\times G \wedge \text{IsPartOrder}(G,r) \wedge (\forall g\in G.\ \forall a b.\ \)
\( \langle a,b\rangle \in r \longrightarrow \langle P\langle a,g\rangle ,P\langle b,g\rangle \rangle \in r \wedge \langle P\langle g,a\rangle ,P\langle g,b\rangle \rangle \in r ) ) \)
theorem group0_2_T2:
assumes \( \text{IsAgroup}(G,f) \)
shows \( \text{GroupInv}(G,f) : G\rightarrow G \)Definition of AbsoluteValue:
\( \text{AbsoluteValue}(G,P,r) \equiv id( \text{Nonnegative}(G,P,r)) \cup \)
\( \text{restrict}( \text{GroupInv}(G,P),G - \text{Nonnegative}(G,P,r)) \)
lemma func1_1_L1:
assumes \( f:A\rightarrow C \)
shows \( domain(f) = A \) lemma (in group3) OrderedGroup_ZF_1_L3A: shows \( 1 \in G^+ \)
lemma (in group3) OrderedGroup_ZF_3_L2:
assumes \( a\in G^+ \)
shows \( \vert a\vert = a \)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 Nonnegative:
\( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)
lemma (in group3) OrderedGroup_ZF_3_L2A: shows \( \vert 1 \vert = 1 \)
lemma (in group3) OrderedGroup_ZF_1_L1: shows \( group0(G,P) \)
lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
lemma (in group3) OrderedGroup_ZF_1_L4C:
assumes \( a\leq 1 \) and \( a\neq 1 \)
shows \( a \in G-G^+ \) lemma (in group3) OrderedGroup_ZF_3_L3:
assumes \( a \in G-G^+ \)
shows \( \vert a\vert = a^{-1} \) lemma (in group3) OrderedGroup_ZF_1_L6:
assumes \( r \text{ is total on } G \) and \( a\in G-G^+ \)
shows \( a\leq 1 \), \( a^{-1} \in G^+ \), \( \text{restrict}( \text{GroupInv}(G,P),G-G^+)(a) \in G^+ \) lemma (in group3) OrderedGroup_ZF_3_L1: shows \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G \)
lemma (in group3) OrderedGroup_ZF_3_L3B:
assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( \vert a\vert \in G^+ \) lemma func1_1_L1A:
assumes \( f:X\rightarrow Y \) and \( \forall x\in X.\ f(x) \in Z \)
shows \( f:X\rightarrow Z \) lemma (in group0) group0_2_L8A:
assumes \( a\in G \) and \( a^{-1} = 1 \)
shows \( a = 1 \) lemma (in group3) OrderedGroup_ZF_1_L2: shows \( g\in G^+ \longleftrightarrow 1 \leq g \)
lemma (in group3) OrderedGroup_ZF_1_L4:
assumes \( a\leq b \)
shows \( a\in G \), \( b\in G \) lemma (in group3) OrderedGroup_ZF_1_L3:
assumes \( g\in G \)
shows \( g\leq g \) lemma (in group3) OrderedGroup_ZF_1_L4B:
assumes \( r \text{ is total on } G \) and \( a\in G^+ \) and \( b \in G-G^+ \)
shows \( b\leq a \) lemma (in group3) OrderedGroup_ZF_1_L5:
assumes \( a\leq b \)
shows \( b^{-1}\leq a^{-1} \) lemma (in group3) Group_order_transitive:
assumes \( a\leq b \), \( b\leq c \)
shows \( a\leq c \)Definition of IsPartOrder:
\( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)
lemma (in group3) OrderedGroup_ZF_3_L5:
assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( a \leq \vert a\vert \) lemma (in group3) OrderedGroup_ZF_3_L6:
assumes \( a\in G \)
shows \( a^{-1} \leq \vert a\vert \) lemma (in group3) OrderedGroup_ZF_1_L5B:
assumes \( a\leq b \) and \( c\leq d \)
shows \( a\cdot c \leq b\cdot d \) lemma (in group0) group_inv_of_inv:
assumes \( a\in G \)
shows \( a = (a^{-1})^{-1} \) lemma (in group3) OrderedGroup_ZF_3_L4:
assumes \( a\leq b \) and \( a^{-1}\leq b \)
shows \( \vert a\vert \leq b \) lemma (in group0) inverse_in_group:
assumes \( x\in G \)
shows \( x^{-1}\in G \) lemma (in group3) OrderedGroup_ZF_3_L7:
assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( \vert a^{-1}\vert \leq \vert a\vert \) lemma (in group3) group_order_antisym:
assumes \( a\leq b \), \( b\leq a \)
shows \( a=b \) lemma (in group0) group0_2_L1: shows \( monoid0(G,P) \)
lemma (in monoid0) group0_1_L1:
assumes \( a\in G \), \( b\in G \)
shows \( a\oplus b \in G \) lemma (in group3) OrderedGroup_ZF_3_L7A:
assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( \vert a^{-1}\vert = \vert a\vert \) lemma (in group0) group0_2_L12:
assumes \( a\in G \), \( b\in G \)
shows \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \) lemma (in group0) group_inv_of_two:
assumes \( a\in G \) and \( b\in G \)
shows \( b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} \)Definition of IsCommutative:
\( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
theorem (in group3) OrdGroup_triangle_ineq:
assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \)
shows \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \) lemma (in group3) OrderedGroup_ZF_3_L7C:
assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \), \( a\in G \), \( b\in G \) and \( \vert a\vert \leq c \), \( \vert b\vert \leq d \)
shows \( \vert a\cdot b\vert \leq c\cdot d \) lemma (in group0) group_op_closed:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b \in G \) lemma (in group0) inv_cancel_two:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \) lemma (in group3) OrderedGroup_ZF_1_L5C:
assumes \( c\in G \) and \( a\leq b\cdot c \) and \( b\leq b_1 \)
shows \( a\leq b_1\cdot c \) lemma (in group3) OrderedGroup_ZF_1_L5H:
assumes \( a\in G \), \( b\in G \) and \( a\cdot b^{-1} \leq c \)
shows \( a \leq c\cdot b \), \( c^{-1}\cdot a \leq b \) lemma (in group3) OrderedGroup_ZF_3_L7D:
assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \vert a\cdot b^{-1}\vert \leq c \)
shows \( \vert a\vert \leq c\cdot \vert b\vert \), \( \vert a\vert \leq \vert b\vert \cdot c \), \( c^{-1}\cdot a \leq b \), \( a\cdot c^{-1} \leq b \), \( a \leq b\cdot c \) lemma (in group3) OrdGroup_triangle_ineq3:
assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)
shows \( \vert a\cdot b\cdot c\vert \leq \vert a\vert \cdot \vert b\vert \cdot \vert c\vert \) lemma (in group0) group0_4_L8:
assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)
shows \( a\cdot (b\cdot c)^{-1} = (a\cdot d^{-1}\cdot c^{-1})\cdot (d\cdot b^{-1}) \), \( a\cdot b\cdot (c\cdot d) = c\cdot a\cdot (b\cdot d) \), \( a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d) \), \( a\cdot (b\cdot c^{-1})\cdot d = a\cdot b\cdot d\cdot c^{-1} \), \( (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1} \) lemma (in group3) OrderedGroup_ZF_3_L8:
assumes \( a\in G \) and \( \vert a\vert \leq L \)
shows \( L^{-1}\leq a \) lemma (in group3) OrderedGroup_ZF_1_L5AB:
assumes \( 1 \leq a \)
shows \( a^{-1}\leq 1 \) and \( \neg (a\leq 1 \wedge a\neq 1 ) \) lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
lemma (in group3) OrderedGroup_ZF_1_L9C:
assumes \( a\in G \), \( b\in G \) and \( c\leq a\cdot b \)
shows \( c\cdot b^{-1} \leq a \), \( a^{-1}\cdot c \leq b \) lemma (in group3) OrderedGroup_ZF_1_L9:
assumes \( a\in G \), \( b\in G \)
shows \( a\leq b \longleftrightarrow a\cdot b^{-1} \leq 1 \) lemma (in group0) group0_2_L6:
assumes \( x\in G \)
shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \) lemma (in group3) OrderedGroup_ZF_3_L8A:
assumes \( r \text{ is total on } G \) and \( a\in G \) and \( \vert a\vert \leq L \)
shows \( a\leq L \), \( 1 \leq L \)Definition of IsBoundedAbove:
\( \text{IsBoundedAbove}(A,r) \equiv ( A=0 \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in r)) \)
Definition of IsBoundedBelow:
\( \text{IsBoundedBelow}(A,r) \equiv (A=0 \vee (\exists l.\ \forall x\in A.\ \langle l,x\rangle \in r)) \)
Definition of IsBounded:
\( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
lemma (in group3) OrderedGroup_ZF_3_L9:
assumes \( r \text{ is total on } G \) and \( A\subseteq G \) and \( \forall a\in A.\ \vert a\vert \leq L \)
shows \( \text{IsBounded}(A,r) \) lemma (in group3) OrderedGroup_ZF_3_L9A:
assumes \( r \text{ is total on } G \) and \( \forall x\in X.\ b(x)\in G \wedge \vert b(x)\vert \leq L \)
shows \( \text{IsBounded}(\{b(x).\ x\in X\},r) \) lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) lemma Order_ZF_3_L2:
assumes \( r \text{ is total on } X \) and \( x\in X \), \( y\in X \)
shows \( \langle x, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle y, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),x\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),y\rangle \in r \) lemma (in group3) OrderedGroup_ZF_1_L4D:
assumes \( a\in G-G^+ \) and \( b\leq a \)
shows \( b\in G-G^+ \) lemma (in group3) OrderedGroup_ZF_3_L10:
assumes \( r \text{ is total on } G \) and \( l\leq a \), \( a\leq u \)
shows \( \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) lemma (in group3) OrderedGroup_ZF_3_L10A:
assumes \( r \text{ is total on } G \) and \( \text{IsBounded}(A,r) \)
shows \( \exists L.\ \forall a\in A.\ \vert a\vert \leq L \) theorem (in group3) ord_group_fin_bounded:
assumes \( r \text{ is total on } G \) and \( B\in Fin(G) \)
shows \( \text{IsBounded}(B,r) \) lemma (in group3) OrderedGroup_ZF_3_L11:
assumes \( r \text{ is total on } G \) and \( \text{IsBounded}(\{b(x).\ x\in X\},r) \)
shows \( \exists L.\ \forall x\in X.\ \vert b(x)\vert \leq L \) lemma (in group3) OrderedGroup_ZF_3_L3D:
assumes \( a\in G \) and \( \vert a\vert = 1 \)
shows \( a = 1 \) lemma Order_ZF_4_L3:
assumes \( \text{antisym}(r) \) and \( \text{HasAmaximum}(r,A) \)
shows \( \text{Maximum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \) lemma Order_ZF_4_L4:
assumes \( \text{antisym}(r) \) and \( \text{HasAminimum}(r,A) \)
shows \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \)Definition of GreaterOf:
\( \text{GreaterOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }b\text{ else }a) \)
lemma (in group3) OrderedGroup_ZF_4_L2:
assumes \( r \text{ is total on } G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( a\in A \)
shows \( \vert a\vert \leq \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \) lemma (in group3) OrderedGroup_ZF_4_L1:
assumes \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( M = \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)
shows \( M \in \text{AbsoluteValue}(G,P,r)(A) \) lemma (in group3) OrderedGroup_ZF_4_L3:
assumes \( r \text{ is total on } G \) and \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( b \in \text{AbsoluteValue}(G,P,r)(A) \)
shows \( b\leq \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)Definition of HasAmaximum:
\( \text{HasAmaximum}(r,A) \equiv \exists M\in A.\ \forall x\in A.\ \langle x,M\rangle \in r \)
lemma (in group3) OrderedGroup_ZF_4_L4:
assumes \( r \text{ is total on } G \) and \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \)
shows \( \text{HasAmaximum}(r, \text{AbsoluteValue}(G,P,r)(A)) \) lemma (in group0) group0_2_L9:
assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = 1 \)
shows \( a = b^{-1} \) and \( b = a^{-1} \)Definition of Xor:
\( p \text{ Xor } q \equiv (p\vee q) \wedge \neg (p \wedge q) \)
lemma (in group0) group0_2_L11:
assumes \( a\in G \), \( b\in G \) and \( a^{-1}\cdot b = 1 \)
shows \( a=b \) lemma (in group0) OrderedGroup_ZF_5_L1:
assumes \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)
shows \( \langle a,b\rangle \in r \longleftrightarrow a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \) lemma (in group0) group0_2_L17:
assumes \( H\subseteq G \) and \( H \text{ is closed under } P \)
shows \( (H \cup \{1 \}) \text{ is closed under } P \)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 group0) group0_2_L14A:
assumes \( a\in G \), \( b\in G \), \( c\in G \)
shows \( a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \), \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \), \( a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1} \), \( a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1} \), \( (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1} \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a \), \( a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b \) lemma Fol1_L2:
assumes \( \forall x y z.\ \langle x, y\rangle \in r \wedge \langle y, z\rangle \in r \longrightarrow \langle x, z\rangle \in r \)
shows \( \text{trans}(r) \) lemma (in group0) group0_4_L6D:
assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)
shows \( a\cdot b^{-1}\cdot (a\cdot c^{-1})^{-1} = c\cdot b^{-1} \), \( (a\cdot c)^{-1}\cdot (b\cdot c) = a^{-1}\cdot b \), \( a\cdot (b\cdot (c\cdot a^{-1}\cdot b^{-1})) = c \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot a^{-1}) = b \) lemma (in group0) OrderedGroup_ZF_5_L2:
assumes \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \)
shows \( \text{antisym}(r) \) lemma (in group0) OrderedGroup_ZF_5_L3:
assumes \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and \( H\subseteq G \), \( H \text{ is closed under } P \)
shows \( \text{trans}(r) \) lemma (in group0) OrderedGroup_ZF_5_L4:
assumes \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and \( P \text{ is commutative on } G \) and \( \langle a,b\rangle \in r \) and \( c\in G \)
shows \( \langle a\cdot c,b\cdot c\rangle \in r \wedge \langle c\cdot a,c\cdot b\rangle \in r \) lemma (in group3) OrderedGroup_ZF_1_L24: shows \( G^+ = G_+\cup \{1 \} \)
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 OrderFromPosSet:
\( \text{OrderFromPosSet}(G,P,H) \equiv \)
\( \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee P\langle \text{GroupInv}(G,P)(\text{fst}(p)),\text{snd}(p)\rangle \in H \} \)
lemma (in group0) OrderedGroup_ZF_5_L5:
assumes \( P \text{ is commutative on } G \) and \( H\subseteq G \), \( H \text{ is closed under } P \) and \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \) and \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)
shows \( \text{IsAnOrdGroup}(G,P,r) \), \( r \text{ is total on } G \), \( \text{Nonnegative}(G,P,r) = \text{PositiveSet}(G,P,r) \cup \{1 \} \) lemma (in group0) OrderedGroup_ZF_5_L6:
assumes \( P \text{ is commutative on } G \) and \( H\subseteq G \) and \( 1 \notin H \) and \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)
shows \( \text{PositiveSet}(G,P,r) = H \)Definition of OddExtension:
\( \text{OddExtension}(G,P,r,f) \equiv \)
\( (f \cup \{\langle a, \text{GroupInv}(G,P)(f( \text{GroupInv}(G,P)(a)))\rangle .\ \)
\( a \in \text{GroupInv}(G,P)( \text{PositiveSet}(G,P,r))\} \cup \)
\( \{\langle \text{ TheNeutralElement}(G,P),\text{ TheNeutralElement}(G,P)\rangle \}) \)
lemma (in group3) OrderedGroup_ZF_1_L27:
assumes \( a \in (-G_+) \)
shows \( a^{-1} \in G_+ \) lemma (in group3) OrderedGroup_ZF_6_L2:
assumes \( f: G_+\rightarrow G \) and \( a\in -G_+ \)
shows \( f(a^{-1}) \in G \), \( (f(a^{-1}))^{-1} \in G \) lemma (in group3) OrdGroup_decomp2:
assumes \( r \text{ is total on } G \)
shows \( G = G_+ \cup (-G_+)\cup \{1 \} \), \( G_+\cap (-G_+) = 0 \), \( 1 \notin G_+\cup (-G_+) \) lemma (in group3) OrderedGroup_ZF_6_L1: shows \( f^\circ = f \cup \{\langle a, (f(a^{-1}))^{-1}\rangle .\ a \in -G_+\} \cup \{\langle 1 ,1 \rangle \} \)
lemma func1_1_L11E:
assumes \( f:X\rightarrow Y \) and \( \forall x\in A.\ b(x)\in B \) and \( X\cap A = \emptyset \) and \( a \notin X\cup A \) and \( g = f \cup \{\langle x,b(x)\rangle .\ x\in A\} \cup \{\langle a,c\rangle \} \)
shows \( g : X\cup A\cup \{a\} \rightarrow Y\cup B\cup \{c\} \), \( \forall x\in X.\ g(x) = f(x) \), \( \forall x\in A.\ g(x) = b(x) \), \( g(a) = c \) lemma (in group3) OrderedGroup_ZF_1_L25: shows \( (-G_+) = \{a^{-1}.\ a\in G_+\} \), \( (-G_+) \subseteq G \)
lemma (in group3) odd_ext_props:
assumes \( r \text{ is total on } G \) and \( f: G_+\rightarrow G \)
shows \( f^\circ : G \rightarrow G \), \( \forall a\in G_+.\ (f^\circ )(a) = f(a) \), \( \forall a\in (-G_+).\ (f^\circ )(a) = (f(a^{-1}))^{-1} \), \( (f^\circ )(1 ) = 1 \) lemma (in group3) oddext_is_odd:
assumes \( r \text{ is total on } G \) and \( f: G_+\rightarrow G \) and \( a\in G \)
shows \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \) lemma (in group0) group0_6_L2:
assumes \( p : G\rightarrow G \)
shows \( (\forall a\in G.\ p(a^{-1}) = (p(a))^{-1}) \longleftrightarrow (\forall a\in G.\ (p(a^{-1}))^{-1} = p(a)) \) lemma (in group3) OrderedGroup_ZF_1_L8:
assumes \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \neg (a\leq b) \)
shows \( b \leq a \), \( a^{-1} \leq b^{-1} \), \( a\neq b \), \( b \lt a \) lemma (in group3) OrderedGroup_ZF_2_L2A:
assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( \forall a\in G.\ \exists b\in A.\ a\leq b \)
shows \( \forall a\in G.\ \exists b\in A.\ a\neq b \wedge a\leq b \), \( \neg \text{IsBoundedAbove}(A,r) \), \( A \notin Fin(G) \) lemma Order_ZF_3_L10:
assumes \( \forall a\in A.\ \langle a,u\rangle \in r \)
shows \( \text{IsBoundedAbove}(A,r) \) lemma (in group3) OrderedGroup_ZF_7_L1:
assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) and \( A\subseteq G \) and \( \text{IsBoundedAbove}(f(A),r) \)
shows \( \text{IsBoundedAbove}(A,r) \) lemma func1_1_L18:
assumes \( f:A\rightarrow B \), \( g:B\rightarrow C \), \( h:C\rightarrow D \) and \( x\in A \)
shows \( (h\circ g\circ f)(x) \in D \), \( (h\circ g\circ f)(x) = h(g(f(x))) \) lemma (in group3) OrderedGroup_ZF_1_L5AD:
assumes \( b \in G \) and \( a\leq b^{-1} \)
shows \( b \leq a^{-1} \) lemma (in group3) OrderedGroup_ZF_7_L2:
assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( X\neq 0 \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq f(y) \) and \( \forall x\in X.\ b(x) \in G \wedge f(b(x)) \leq U \)
shows \( \exists u.\ \forall x\in X.\ b(x) \leq u \) lemma (in group3) OrderedGroup_ZF_7_L3:
assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( X\neq 0 \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a \) and \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \)
shows \( \exists l.\ \forall x\in X.\ l \leq b(x) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8