diff options
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal')
6 files changed, 18 insertions, 6 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda index cad9714..aa37d59 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda @@ -63,9 +63,11 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public ; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤ + ; x≈ε⇒x⁻¹≈ε ; x<ε⇒x⁻¹>ε; x>ε⇒x⁻¹<ε ; x≤ε⇒x⁻¹≥ε; x≥ε⇒x⁻¹≤ε + ; x⁻¹≈ε⇒x≈ε ; x⁻¹<ε⇒x>ε; x⁻¹>ε⇒x<ε ; x⁻¹≤ε⇒x≥ε; x⁻¹≥ε⇒x≤ε diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda index 1ccde6f..37996b0 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda @@ -61,8 +61,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public ; -‿anti-mono-<; -‿anti-mono-≤ ; -‿anti-cancel-<; -‿anti-cancel-≤ - ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 - ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 + ; x≈0⇒-x≈0 ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 + ; -x≈0⇒x≈0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 ; x<y⇒0<y-x; 0<y-x⇒x<y diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda index 3961ca1..03e8ecd 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda @@ -61,8 +61,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public ; -‿anti-mono-<; -‿anti-mono-≤ ; -‿anti-cancel-<; -‿anti-cancel-≤ - ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 - ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 + ; x≈0⇒-x≈0 ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 + ; -x≈0⇒x≈0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 ; x<y⇒0<y-x; 0<y-x⇒x<y diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda index f0ae47d..51a054e 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda @@ -61,8 +61,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR ; -‿anti-mono-<; -‿anti-mono-≤ ; -‿anti-cancel-<; -‿anti-cancel-≤ - ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 - ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 + ; x≈0⇒-x≈0 ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 + ; -x≈0⇒x≈0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 ; x<y⇒0<y-x; 0<y-x⇒x<y diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda index cf8e4f2..e186c71 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda @@ -164,6 +164,14 @@ x⁻¹≥ε⇒x≤ε {x} x⁻¹≥ε = begin x ⁻¹ ⁻¹ ≤⟨ x≥ε⇒x⁻¹≤ε x⁻¹≥ε ⟩ ε ∎ +---- Preserves and respects signs (_≈_) + +x≈ε⇒x⁻¹≈ε : ∀ {x} → x ≈ ε → x ⁻¹ ≈ ε +x≈ε⇒x⁻¹≈ε {x} x≈ε = ≮∧≯⇒≈ (<-irrefl (Eq.sym x≈ε) ∘ x⁻¹<ε⇒x>ε) (<-irrefl x≈ε ∘ x⁻¹>ε⇒x<ε) + +x⁻¹≈ε⇒x≈ε : ∀ {x} → x ⁻¹ ≈ ε → x ≈ ε +x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = ≮∧≯⇒≈ (<-irrefl (Eq.sym x⁻¹≈ε) ∘ x<ε⇒x⁻¹>ε) (<-irrefl x⁻¹≈ε ∘ x>ε⇒x⁻¹<ε) + -- ---- Infer signs -- -- _≈_ diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda index db070e0..c83f683 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda @@ -105,11 +105,13 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelian ; ⁻¹-anti-cancel-< to -‿anti-cancel-< ; ⁻¹-anti-cancel-≤ to -‿anti-cancel-≤ + ; x≈ε⇒x⁻¹≈ε to x≈0⇒-x≈0 ; x<ε⇒x⁻¹>ε to x<0⇒-x>0 ; x>ε⇒x⁻¹<ε to x>0⇒-x<0 ; x≤ε⇒x⁻¹≥ε to x≤0⇒-x≥0 ; x≥ε⇒x⁻¹≤ε to x≥0⇒-x≤0 + ; x⁻¹≈ε⇒x≈ε to -x≈0⇒x≈0 ; x⁻¹<ε⇒x>ε to -x<0⇒x>0 ; x⁻¹>ε⇒x<ε to -x>0⇒x<0 ; x⁻¹≤ε⇒x≥ε to -x≤0⇒x≥0 |