IsarMathLib

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

theory Real_ZF imports Int_ZF_IML Ring_ZF_1
begin

The goal of the Real_ZF series of theory files is to provide a contruction of the set of real numbers. There are several ways to construct real numbers. Most common start from the rational numbers and use Dedekind cuts or Cauchy sequences. Real_ZF_x.thy series formalizes an alternative approach that constructs real numbers directly from the group of integers. Our formalization is mostly based on \cite{Arthan2004}. Different variants of this contruction are also described in \cite{Campo2003} and \cite{Street2003}. I recommend to read these papers, but for the impatient here is a short description: we take a set of maps \(s : Z\rightarrow Z\) such that the set \(\{s(m+n)-s(m)-s(n)\}_{n,m \in Z}\) is finite (\(Z\) means the integers here). We call these maps slopes. Slopes form a group with the natural addition \((s+r)(n) = s(n)+r(n)\). The maps such that the set \(s(Z)\) is finite (finite range functions) form a subgroup of slopes. The additive group of real numbers is defined as the quotient group of slopes by the (sub)group of finite range functions. The multiplication is defined as the projection of the composition of slopes into the resulting quotient (coset) space.

The definition of real numbers

This section contains the construction of the ring of real numbers as classes of slopes - integer almost homomorphisms. The real definitions are in Group_ZF_2 theory, here we just specialize the definitions of almost homomorphisms, their equivalence and operations to the additive group of integers from the general case of abelian groups considered in Group_ZF_2.

The set of slopes is defined as the set of almost homomorphisms on the additive group of integers.

definition

\( Slopes \equiv \text{AlmostHoms}(int,IntegerAddition) \)

The first operation on slopes (pointwise addition) is a special case of the first operation on almost homomorphisms.

definition

\( SlopeOp1 \equiv \text{AlHomOp1}(int,IntegerAddition) \)

The second operation on slopes (composition) is a special case of the second operation on almost homomorphisms.

definition

\( SlopeOp2 \equiv \text{AlHomOp2}(int,IntegerAddition) \)

Bounded integer maps are functions from integers to integers that have finite range. They play a role of zero in the set of real numbers we are constructing.

definition

\( BoundedIntMaps \equiv \text{FinRangeFunctions}(int,int) \)

Bounded integer maps form a normal subgroup of slopes. The equivalence relation on slopes is the (group) quotient relation defined by this subgroup.

definition

\( SlopeEquivalenceRel \equiv \text{QuotientGroupRel}(Slopes,SlopeOp1,BoundedIntMaps) \)

The set of real numbers is the set of equivalence classes of slopes.

definition

\( RealNumbers \equiv Slopes//SlopeEquivalenceRel \)

The addition on real numbers is defined as the projection of pointwise addition of slopes on the quotient. This means that the additive group of real numbers is the quotient group: the group of slopes (with pointwise addition) defined by the normal subgroup of bounded integer maps.

definition

\( RealAddition \equiv \text{ProjFun2}(Slopes,SlopeEquivalenceRel,SlopeOp1) \)

Multiplication is defined as the projection of composition of slopes on the quotient. The fact that it works is probably the most surprising part of the construction.

definition

\( RealMultiplication \equiv \text{ProjFun2}(Slopes,SlopeEquivalenceRel,SlopeOp2) \)

We first show that we can use theorems proven in some proof contexts (locales). The locale group1 requires assumption that we deal with an abelian group. The next lemma allows to use all theorems proven in the context called group1.

lemma Real_ZF_1_L1:

shows \( group1(int,IntegerAddition) \) using group1_axioms.intro, group1_def, Int_ZF_1_T2

Real numbers form a ring. This is a special case of the theorem proven in Ring_ZF_1.thy, where we show the same in general for almost homomorphisms rather than slopes.

theorem Real_ZF_1_T1:

shows \( \text{IsAring}(RealNumbers,RealAddition,RealMultiplication) \)proof
let \( AH = \text{AlmostHoms}(int,IntegerAddition) \)
let \( Op1 = \text{AlHomOp1}(int,IntegerAddition) \)
let \( FR = \text{FinRangeFunctions}(int,int) \)
let \( Op2 = \text{AlHomOp2}(int,IntegerAddition) \)
let \( R = \text{QuotientGroupRel}(AH,Op1,FR) \)
let \( A = \text{ProjFun2}(AH,R,Op1) \)
let \( M = \text{ProjFun2}(AH,R,Op2) \)
have \( \text{IsAring}(AH//R,A,M) \) using Real_ZF_1_L1, Ring_ZF_1_1_T1
then show \( thesis \) using Slopes_def, SlopeOp2_def, SlopeOp1_def, BoundedIntMaps_def, SlopeEquivalenceRel_def, RealNumbers_def, RealAddition_def, RealMultiplication_def
qed

We can use theorems proven in group0 and group1 contexts applied to the group of real numbers.

lemma Real_ZF_1_L2:

shows \( group0(RealNumbers,RealAddition) \), \( RealAddition \text{ is commutative on } RealNumbers \), \( group1(RealNumbers,RealAddition) \)proof
have \( \text{IsAgroup}(RealNumbers,RealAddition) \), \( RealAddition \text{ is commutative on } RealNumbers \) using Real_ZF_1_T1, IsAring_def
then show \( group0(RealNumbers,RealAddition) \), \( RealAddition \text{ is commutative on } RealNumbers \), \( group1(RealNumbers,RealAddition) \) using group1_axioms.intro, group0_def, group1_def
qed

Let's define some notation.

locale real0

defines \( \mathbb{R} \equiv RealNumbers \)

defines \( a + b \equiv RealAddition\langle a,b\rangle \)

defines \( - a \equiv \text{GroupInv}(\mathbb{R} ,RealAddition)(a) \)

defines \( a - b \equiv a + ( - b) \)

defines \( a\cdot b \equiv RealMultiplication\langle a,b\rangle \)

defines \( 0 \equiv \text{ TheNeutralElement}(RealNumbers,RealAddition) \)

defines \( 1 \equiv \text{ TheNeutralElement}(RealNumbers,RealMultiplication) \)

defines \( 2 \equiv 1 + 1 \)

defines \( \mathbb{R} _0 \equiv \mathbb{R} -\{ 0 \} \)

defines \( a^{-1} \equiv \text{GroupInv}(\mathbb{R} _0,\text{restrict}(RealMultiplication,\mathbb{R} _0\times \mathbb{R} _0))(a) \)

In real0 context all theorems proven in the ring0, context are valid.

lemma (in real0) Real_ZF_1_L3:

shows \( ring0(\mathbb{R} ,RealAddition,RealMultiplication) \) using Real_ZF_1_T1, ring0_def, Ring_ZF_1_L1

Lets try out our notation to see that zero and one are real numbers.

lemma (in real0) Real_ZF_1_L4:

shows \( 0 \in \mathbb{R} \), \( 1 \in \mathbb{R} \) using Real_ZF_1_L3, Ring_ZF_1_L2

The lemma below lists some properties that require one real number to state.

lemma (in real0) Real_ZF_1_L5:

assumes A1: \( a\in \mathbb{R} \)

shows \( ( - a) \in \mathbb{R} \), \( ( - ( - a)) = a \), \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( a - a = 0 \), \( a - 0 = a \) using assms, Real_ZF_1_L3, Ring_ZF_1_L3

The lemma below lists some properties that require two real numbers to state.

lemma (in real0) Real_ZF_1_L6:

assumes \( a\in \mathbb{R} \), \( b\in \mathbb{R} \)

shows \( a + b \in \mathbb{R} \), \( a - b \in \mathbb{R} \), \( a\cdot b \in \mathbb{R} \), \( a + b = b + a \), \( ( - a)\cdot b = - (a\cdot b) \), \( a\cdot ( - b) = - (a\cdot b) \) using assms, Real_ZF_1_L3, Ring_ZF_1_L4, Ring_ZF_1_L7

Multiplication of reals is associative.

lemma (in real0) Real_ZF_1_L6A:

assumes \( a\in \mathbb{R} \), \( b\in \mathbb{R} \), \( c\in \mathbb{R} \)

shows \( a\cdot (b\cdot c) = (a\cdot b)\cdot c \) using assms, Real_ZF_1_L3, Ring_ZF_1_L11

Addition is distributive with respect to multiplication.

lemma (in real0) Real_ZF_1_L7:

assumes \( a\in \mathbb{R} \), \( b\in \mathbb{R} \), \( c\in \mathbb{R} \)

shows \( a\cdot (b + c) = a\cdot b + a\cdot c \), \( (b + c)\cdot a = b\cdot a + c\cdot a \), \( a\cdot (b - c) = a\cdot b - a\cdot c \), \( (b - c)\cdot a = b\cdot a - c\cdot a \) using assms, Real_ZF_1_L3, ring_oper_distr, Ring_ZF_1_L8

A simple rearrangement with four real numbers.

lemma (in real0) Real_ZF_1_L7A:

assumes \( a\in \mathbb{R} \), \( b\in \mathbb{R} \), \( c\in \mathbb{R} \), \( d\in \mathbb{R} \)

shows \( a - b + (c - d) = a + c - b - d \) using assms, Real_ZF_1_L2, group0_4_L8A

RealAddition is defined as the projection of the first operation on slopes (that is, slope addition) on the quotient (slopes divided by the "almost equal" relation. The next lemma plays with definitions to show that this is the same as the operation induced on the appriopriate quotient group. The names AH, Op1 and FR are used in group1 context to denote almost homomorphisms, the first operation on AH and finite range functions resp.

lemma Real_ZF_1_L8:

assumes \( AH = \text{AlmostHoms}(int,IntegerAddition) \) and \( Op1 = \text{AlHomOp1}(int,IntegerAddition) \) and \( FR = \text{FinRangeFunctions}(int,int) \)

shows \( RealAddition = \text{QuotientGroupOp}(AH,Op1,FR) \) using assms, RealAddition_def, SlopeEquivalenceRel_def, QuotientGroupOp_def, Slopes_def, SlopeOp1_def, BoundedIntMaps_def

The symbol \( 0 \) in the real0 context is defined as the neutral element of real addition. The next lemma shows that this is the same as the neutral element of the appriopriate quotient group.

lemma (in real0) Real_ZF_1_L9:

assumes \( AH = \text{AlmostHoms}(int,IntegerAddition) \) and \( Op1 = \text{AlHomOp1}(int,IntegerAddition) \) and \( FR = \text{FinRangeFunctions}(int,int) \) and \( r = \text{QuotientGroupRel}(AH,Op1,FR) \)

shows \( \text{ TheNeutralElement}(AH//r, \text{QuotientGroupOp}(AH,Op1,FR)) = 0 \), \( SlopeEquivalenceRel = r \) using assms, Slopes_def, Real_ZF_1_L8, RealNumbers_def, SlopeEquivalenceRel_def, SlopeOp1_def, BoundedIntMaps_def

Zero is the class of any finite range function.

lemma (in real0) Real_ZF_1_L10:

assumes A1: \( s \in Slopes \)

shows \( SlopeEquivalenceRel\{s\} = 0 \longleftrightarrow s \in BoundedIntMaps \)proof
let \( AH = \text{AlmostHoms}(int,IntegerAddition) \)
let \( Op1 = \text{AlHomOp1}(int,IntegerAddition) \)
let \( FR = \text{FinRangeFunctions}(int,int) \)
let \( r = \text{QuotientGroupRel}(AH,Op1,FR) \)
let \( e = \text{ TheNeutralElement}(AH//r, \text{QuotientGroupOp}(AH,Op1,FR)) \)
from A1 have \( group1(int,IntegerAddition) \), \( s\in AH \) using Real_ZF_1_L1, Slopes_def
then have \( r\{s\} = e \longleftrightarrow s \in FR \) using Group_ZF_3_3_L5
moreover
have \( r = SlopeEquivalenceRel \), \( e = 0 \), \( FR = BoundedIntMaps \) using SlopeEquivalenceRel_def, Slopes_def, SlopeOp1_def, BoundedIntMaps_def, Real_ZF_1_L9
ultimately show \( thesis \)
qed

We will need a couple of results from Group_ZF_3.thy The first two that state that the definition of addition and multiplication of real numbers are consistent, that is the result does not depend on the choice of the slopes representing the numbers. The second one implies that what we call SlopeEquivalenceRel is actually an equivalence relation on the set of slopes. We also show that the neutral element of the multiplicative operation on reals (in short number \(1\)) is the class of the identity function on integers.

lemma Real_ZF_1_L11:

shows \( \text{Congruent2}(SlopeEquivalenceRel,SlopeOp1) \), \( \text{Congruent2}(SlopeEquivalenceRel,SlopeOp2) \), \( SlopeEquivalenceRel \subseteq Slopes \times Slopes \), \( \text{equiv}(Slopes, SlopeEquivalenceRel) \), \( SlopeEquivalenceRel\{id(int)\} = \) \( \text{ TheNeutralElement}(RealNumbers,RealMultiplication) \), \( BoundedIntMaps \subseteq Slopes \)proof
let \( G = int \)
let \( f = IntegerAddition \)
let \( AH = \text{AlmostHoms}(int,IntegerAddition) \)
let \( Op1 = \text{AlHomOp1}(int,IntegerAddition) \)
let \( Op2 = \text{AlHomOp2}(int,IntegerAddition) \)
let \( FR = \text{FinRangeFunctions}(int,int) \)
let \( R = \text{QuotientGroupRel}(AH,Op1,FR) \)
have \( \text{Congruent2}(R,Op1) \), \( \text{Congruent2}(R,Op2) \) using Real_ZF_1_L1, Group_ZF_3_4_L13A, Group_ZF_3_3_L4
then show \( \text{Congruent2}(SlopeEquivalenceRel,SlopeOp1) \), \( \text{Congruent2}(SlopeEquivalenceRel,SlopeOp2) \) using SlopeEquivalenceRel_def, SlopeOp1_def, Slopes_def, BoundedIntMaps_def, SlopeOp2_def
have \( \text{equiv}(AH,R) \) using Real_ZF_1_L1, Group_ZF_3_3_L3
then show \( \text{equiv}(Slopes,SlopeEquivalenceRel) \) using BoundedIntMaps_def, SlopeEquivalenceRel_def, SlopeOp1_def, Slopes_def
then show \( SlopeEquivalenceRel \subseteq Slopes \times Slopes \) using equiv_type
have \( R\{id(int)\} = \text{ TheNeutralElement}(AH//R, \text{ProjFun2}(AH,R,Op2)) \) using Real_ZF_1_L1, Group_ZF_3_4_T2
then show \( SlopeEquivalenceRel\{id(int)\} = \) \( \text{ TheNeutralElement}(RealNumbers,RealMultiplication) \) using Slopes_def, RealNumbers_def, SlopeEquivalenceRel_def, SlopeOp1_def, BoundedIntMaps_def, RealMultiplication_def, SlopeOp2_def
have \( FR \subseteq AH \) using Real_ZF_1_L1, Group_ZF_3_3_L1
then show \( BoundedIntMaps \subseteq Slopes \) using BoundedIntMaps_def, Slopes_def
qed

A one-side implication of the equivalence from Real_ZF_1_L10: the class of a bounded integer map is the real zero.

lemma (in real0) Real_ZF_1_L11A:

assumes \( s \in BoundedIntMaps \)

shows \( SlopeEquivalenceRel\{s\} = 0 \) using assms, Real_ZF_1_L11, Real_ZF_1_L10

The next lemma is rephrases the result from Group_ZF_3.thy that says that the negative (the group inverse with respect to real addition) of the class of a slope is the class of that slope composed with the integer additive group inverse. The result and proof is not very readable as we use mostly generic set theory notation with long names here. Real_ZF_1.thy contains the same statement written in a more readable notation: \([-s] = -[s]\).

lemma (in real0) Real_ZF_1_L12:

assumes A1: \( s \in Slopes \) and Dr: \( r = \text{QuotientGroupRel}(Slopes,SlopeOp1,BoundedIntMaps) \)

shows \( r\{ \text{GroupInv}(int,IntegerAddition)\circ s\} = - (r\{s\}) \)proof
let \( G = int \)
let \( f = IntegerAddition \)
let \( AH = \text{AlmostHoms}(int,IntegerAddition) \)
let \( Op1 = \text{AlHomOp1}(int,IntegerAddition) \)
let \( FR = \text{FinRangeFunctions}(int,int) \)
let \( F = \text{ProjFun2}(Slopes,r,SlopeOp1) \)
from A1, Dr have \( group1(G, f) \), \( s \in \text{AlmostHoms}(G, f) \), \( r = \text{QuotientGroupRel}(\) \( \text{AlmostHoms}(G, f), \text{AlHomOp1}(G, f), \text{FinRangeFunctions}(G, G)) \) and \( F = \text{ProjFun2}( \text{AlmostHoms}(G, f), r, \text{AlHomOp1}(G, f)) \) using Real_ZF_1_L1, Slopes_def, SlopeOp1_def, BoundedIntMaps_def
then have \( r\{ \text{GroupInv}(G, f)\circ s\} =\) \( \text{GroupInv}( \text{AlmostHoms}(G, f) // r, F)(r \{s\}) \) using Group_ZF_3_3_L6
with Dr show \( thesis \) using RealNumbers_def, Slopes_def, SlopeEquivalenceRel_def, RealAddition_def
qed

Two classes are equal iff the slopes that represent them are almost equal.

lemma Real_ZF_1_L13:

assumes \( s \in Slopes \), \( p \in Slopes \) and \( r = SlopeEquivalenceRel \)

shows \( r\{s\} = r\{p\} \longleftrightarrow \langle s,p\rangle \in r \) using assms, Real_ZF_1_L11, eq_equiv_class, equiv_class_eq

Identity function on integers is a slope. This lemma concludes the easy part of the construction that follows from the fact that slope equivalence classes form a ring. It is easy to see that multiplication of classes of almost homomorphisms is not commutative in general. The remaining properties of real numbers, like commutativity of multiplication and the existence of multiplicative inverses have to be proven using properties of the group of integers, rather that in general setting of abelian groups. This is done in the Real_ZF_1 theory.

lemma Real_ZF_1_L14:

shows \( id(int) \in Slopes \)proof
have \( id(int) \in \text{AlmostHoms}(int,IntegerAddition) \) using Real_ZF_1_L1, Group_ZF_3_4_L15
then show \( thesis \) using Slopes_def
qed
end
theorem Int_ZF_1_T2: shows \( \text{IsAgroup}(int,IntegerAddition) \), \( IntegerAddition \text{ is commutative on } int \), \( group0(int,IntegerAddition) \)
lemma Real_ZF_1_L1: shows \( group1(int,IntegerAddition) \)
theorem (in group1) Ring_ZF_1_1_T1:

assumes \( R = \text{QuotientGroupRel}(AH,Op1,FR) \) and \( A = \text{ProjFun2}(AH,R,Op1) \), \( M = \text{ProjFun2}(AH,R,Op2) \)

shows \( \text{IsAring}(AH//R,A,M) \)
Definition of Slopes: \( Slopes \equiv \text{AlmostHoms}(int,IntegerAddition) \)
Definition of SlopeOp2: \( SlopeOp2 \equiv \text{AlHomOp2}(int,IntegerAddition) \)
Definition of SlopeOp1: \( SlopeOp1 \equiv \text{AlHomOp1}(int,IntegerAddition) \)
Definition of BoundedIntMaps: \( BoundedIntMaps \equiv \text{FinRangeFunctions}(int,int) \)
Definition of SlopeEquivalenceRel: \( SlopeEquivalenceRel \equiv \text{QuotientGroupRel}(Slopes,SlopeOp1,BoundedIntMaps) \)
Definition of RealNumbers: \( RealNumbers \equiv Slopes//SlopeEquivalenceRel \)
Definition of RealAddition: \( RealAddition \equiv \text{ProjFun2}(Slopes,SlopeEquivalenceRel,SlopeOp1) \)
Definition of RealMultiplication: \( RealMultiplication \equiv \text{ProjFun2}(Slopes,SlopeEquivalenceRel,SlopeOp2) \)
theorem Real_ZF_1_T1: shows \( \text{IsAring}(RealNumbers,RealAddition,RealMultiplication) \)
Definition of IsAring: \( \text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge \) \( \text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M) \)
lemma (in ring0) Ring_ZF_1_L1: shows \( monoid0(R,M) \), \( group0(R,A) \), \( A \text{ is commutative on } R \)
lemma (in real0) Real_ZF_1_L3: shows \( ring0(\mathbb{R} ,RealAddition,RealMultiplication) \)
lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \)
lemma (in ring0) Ring_ZF_1_L3:

assumes \( a\in R \)

shows \( ( - a) \in R \), \( ( - ( - a)) = a \), \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( a - a = 0 \), \( a - 0 = a \), \( 2 \cdot a = a + a \), \( ( - a) + a = 0 \)
lemma (in ring0) Ring_ZF_1_L4:

assumes \( a\in R \), \( b\in R \)

shows \( a + b \in R \), \( a - b \in R \), \( a\cdot b \in R \), \( a + b = b + a \)
lemma (in ring0) Ring_ZF_1_L7:

assumes \( a\in R \), \( b\in R \)

shows \( ( - a)\cdot b = - (a\cdot b) \), \( a\cdot ( - b) = - (a\cdot b) \), \( ( - a)\cdot b = a\cdot ( - b) \)
lemma (in ring0) Ring_ZF_1_L11:

assumes \( a\in R \), \( b\in R \), \( c\in R \)

shows \( a + b + c = a + (b + c) \), \( a\cdot b\cdot c = a\cdot (b\cdot c) \)
lemma (in ring0) ring_oper_distr:

assumes \( a\in R \), \( b\in R \), \( c\in R \)

shows \( a\cdot (b + c) = a\cdot b + a\cdot c \), \( (b + c)\cdot a = b\cdot a + c\cdot a \)
lemma (in ring0) Ring_ZF_1_L8:

assumes \( a\in R \), \( b\in R \), \( c\in R \)

shows \( a\cdot (b - c) = a\cdot b - a\cdot c \), \( (b - c)\cdot a = b\cdot a - c\cdot a \)
lemma Real_ZF_1_L2: shows \( group0(RealNumbers,RealAddition) \), \( RealAddition \text{ is commutative on } RealNumbers \), \( group1(RealNumbers,RealAddition) \)
lemma (in group0) group0_4_L8A:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b^{-1}\cdot (c\cdot d^{-1}) = a\cdot c\cdot (b^{-1}\cdot d^{-1}) \), \( a\cdot b^{-1}\cdot (c\cdot d^{-1}) = a\cdot c\cdot b^{-1}\cdot d^{-1} \)
Definition of QuotientGroupOp: \( \text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P) \)
lemma Real_ZF_1_L8:

assumes \( AH = \text{AlmostHoms}(int,IntegerAddition) \) and \( Op1 = \text{AlHomOp1}(int,IntegerAddition) \) and \( FR = \text{FinRangeFunctions}(int,int) \)

shows \( RealAddition = \text{QuotientGroupOp}(AH,Op1,FR) \)
lemma (in group1) Group_ZF_3_3_L5:

assumes \( s \in AH \) and \( r = \text{QuotientGroupRel}(AH,Op1,FR) \) and \( \text{ TheNeutralElement}(AH//r, \text{QuotientGroupOp}(AH,Op1,FR)) = e \)

shows \( r\{s\} = e \longleftrightarrow s \in FR \)
lemma (in real0) Real_ZF_1_L9:

assumes \( AH = \text{AlmostHoms}(int,IntegerAddition) \) and \( Op1 = \text{AlHomOp1}(int,IntegerAddition) \) and \( FR = \text{FinRangeFunctions}(int,int) \) and \( r = \text{QuotientGroupRel}(AH,Op1,FR) \)

shows \( \text{ TheNeutralElement}(AH//r, \text{QuotientGroupOp}(AH,Op1,FR)) = 0 \), \( SlopeEquivalenceRel = r \)
lemma (in group1) Group_ZF_3_4_L13A: shows \( \text{Congruent2}( \text{QuotientGroupRel}(AH,Op1,FR),Op2) \)
lemma (in group1) Group_ZF_3_3_L4: shows \( \text{Congruent2}( \text{QuotientGroupRel}(AH,Op1,FR),Op1) \)
lemma (in group1) Group_ZF_3_3_L3: shows \( \text{QuotientGroupRel}(AH,Op1,FR) \subseteq AH \times AH \) and \( \text{equiv}(AH, \text{QuotientGroupRel}(AH,Op1,FR)) \)
theorem (in group1) Group_ZF_3_4_T2:

assumes \( R = \text{QuotientGroupRel}(AH,Op1,FR) \)

shows \( \text{IsAmonoid}(AH//R, \text{ProjFun2}(AH,R,Op2)) \), \( R\{id(G)\} = \text{ TheNeutralElement}(AH//R, \text{ProjFun2}(AH,R,Op2)) \)
lemma (in group1) Group_ZF_3_3_L1: shows \( FR \subseteq AH \)
lemma Real_ZF_1_L11: shows \( \text{Congruent2}(SlopeEquivalenceRel,SlopeOp1) \), \( \text{Congruent2}(SlopeEquivalenceRel,SlopeOp2) \), \( SlopeEquivalenceRel \subseteq Slopes \times Slopes \), \( \text{equiv}(Slopes, SlopeEquivalenceRel) \), \( SlopeEquivalenceRel\{id(int)\} = \) \( \text{ TheNeutralElement}(RealNumbers,RealMultiplication) \), \( BoundedIntMaps \subseteq Slopes \)
lemma (in real0) Real_ZF_1_L10:

assumes \( s \in Slopes \)

shows \( SlopeEquivalenceRel\{s\} = 0 \longleftrightarrow s \in BoundedIntMaps \)
lemma (in group1) Group_ZF_3_3_L6:

assumes \( s \in AH \) and \( r = \text{QuotientGroupRel}(AH,Op1,FR) \) and \( F = \text{ProjFun2}(AH,r,Op1) \)

shows \( r\{\sim s\} = \text{GroupInv}(AH//r,F)(r\{s\}) \)
lemma (in group1) Group_ZF_3_4_L15: shows \( id(G) \in AH \)