diff --git a/Everything/Safe.agda b/Everything/Safe.agda index 86c8b4d..7887c60 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -16,6 +16,7 @@ open import Numbers.Modulo.Group open import Numbers.Integers.Integers open import Numbers.Integers.RingStructure.EuclideanDomain +open import Numbers.Integers.RingStructure.Archimedean open import Numbers.ClassicalReals.Examples open import Numbers.ClassicalReals.RealField.Lemmas @@ -52,12 +53,15 @@ open import Groups.LectureNotes.Lecture1 open import Fields.Fields open import Fields.Orders.Partial.Definition open import Fields.Orders.Total.Definition +open import Fields.Orders.Total.Archimedean open import Fields.Orders.LeastUpperBounds.Examples open import Fields.Orders.Lemmas open import Fields.Orders.Limits.Definition open import Fields.FieldOfFractions.Field open import Fields.FieldOfFractions.Lemmas open import Fields.FieldOfFractions.Order +open import Fields.FieldOfFractions.Order +--open import Fields.FieldOfFractions.Archimedean open import Rings.Definition open import Rings.Lemmas @@ -100,7 +104,7 @@ open import Rings.Orders.Total.BaseExpansion open import Setoids.Setoids open import Setoids.DirectSum open import Setoids.Lists -open import Setoids.Orders +open import Setoids.Orders.Total.Lemmas open import Setoids.Functions.Definition open import Setoids.Functions.Extension open import Setoids.Algebra.Lemmas @@ -159,8 +163,7 @@ open import Modules.PolynomialModule open import Modules.Lemmas open import Modules.DirectSum -open import Fields.CauchyCompletion.Ring -open import Fields.CauchyCompletion.Comparison +open import Fields.CauchyCompletion.Archimedean open import Fields.Orders.Limits.Lemmas open import ProjectEuler.Problem1 diff --git a/Fields/CauchyCompletion/Addition.agda b/Fields/CauchyCompletion/Addition.agda index 1e8ca63..b955606 100644 --- a/Fields/CauchyCompletion/Addition.agda +++ b/Fields/CauchyCompletion/Addition.agda @@ -9,7 +9,8 @@ open import Groups.Lemmas open import Fields.Fields open import Sets.EquivalenceRelations open import Sequences -open import Setoids.Orders +open import Setoids.Orders.Partial.Definition +open import Setoids.Orders.Total.Definition open import Functions open import LogicalFormulae open import Numbers.Naturals.Semiring @@ -31,7 +32,9 @@ open import Fields.Lemmas F open import Fields.CauchyCompletion.Definition order F open import Rings.Orders.Partial.Lemmas pRing open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order }) +open import Rings.Orders.Total.AbsoluteValue order open import Rings.Orders.Total.Lemmas order +open import Rings.Orders.Total.Cauchy order open import Rings.InitialRing R private @@ -39,19 +42,23 @@ private lemm zero a b = refl lemm (succ m) a b = lemm m (Sequence.tail a) (Sequence.tail b) +private + additionConverges : (a b : CauchyCompletion) → cauchy (apply _+_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) + additionConverges record { elts = a ; converges = convA } record { elts = b ; converges = convB } ε 0