blob: 7972c4fd1edbe1dfa2f20327c6fe7d5f296f58bb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Algebraic properties of ordered abelian groups
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Helium.Algebra.Ordered.StrictTotal.Bundles
module Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup
{ℓ₁ ℓ₂ ℓ₃}
(abelianGroup : AbelianGroup ℓ₁ ℓ₂ ℓ₃)
where
open AbelianGroup abelianGroup
renaming
( trans to <-trans
; irrefl to <-irrefl
; asym to <-asym
)
open import Relation.Binary.Core
open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
open import Algebra.Properties.AbelianGroup Unordered.abelianGroup public
open import Algebra.Properties.CommutativeMonoid.Mult.TCOptimised Unordered.commutativeMonoid public
open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public
using
( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-<
; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤
; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-<
; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤
-- _∙_ pres signs
; x≥ε∧y>ε⇒x∙y>ε; x>ε∧y≥ε⇒x∙y>ε
; x≤ε∧y<ε⇒x∙y<ε; x<ε∧y≤ε⇒x∙y<ε
; x≥ε∧y≥ε⇒x∙y≥ε; x≤ε∧y≤ε⇒x∙y≤ε
-- _∙_ resp signs
; x≤ε∧x∙y>ε⇒y>ε; x≤ε∧y∙x>ε⇒y>ε
; x<ε∧x∙y≥ε⇒y>ε; x<ε∧y∙x≥ε⇒y>ε
; x≥ε∧x∙y<ε⇒y<ε; x≥ε∧y∙x<ε⇒y<ε
; x>ε∧x∙y≤ε⇒y<ε; x>ε∧y∙x≤ε⇒y<ε
; x≤ε∧x∙y≥ε⇒y≥ε; x≤ε∧y∙x≥ε⇒y≥ε
; x≥ε∧x∙y≤ε⇒y≤ε; x≥ε∧y∙x≤ε⇒y≤ε
; ×-zeroˡ; ×-zeroʳ
; ×-identityˡ
; n≢0⇒×-monoˡ-<; x>ε⇒×-monoʳ-<; x<ε⇒×-anti-monoʳ-<
; ×-monoˡ-≤; x≥ε⇒×-monoʳ-≤; x≤ε⇒×-anti-monoʳ-≤
; ×-cancelˡ-<; x≥ε⇒×-cancelʳ-<; x≤ε⇒×-anti-cancelʳ-<
; n≢0⇒×-cancelˡ-≤; x>ε⇒×-cancelʳ-≤; x<ε⇒×-anti-cancelʳ-≤
-- _×_ pres signs
; n≢0∧x>ε⇒n×x>ε; n≢0∧x<ε⇒n×x<ε
; x≥ε⇒n×x≥ε; x≤ε⇒n×x≤ε
-- _×_ resp signs
; n×x>ε⇒x>ε; n×x<ε⇒x<ε
; n≢0∧n×x≥ε⇒x≥ε; n≢0∧n×x≤ε⇒x≤ε
; ⁻¹-anti-mono-<; ⁻¹-anti-mono-≤
; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤
; x≈ε⇒x⁻¹≈ε
; x<ε⇒x⁻¹>ε; x>ε⇒x⁻¹<ε
; x≤ε⇒x⁻¹≥ε; x≥ε⇒x⁻¹≤ε
; x⁻¹≈ε⇒x≈ε
; x⁻¹<ε⇒x>ε; x⁻¹>ε⇒x<ε
; x⁻¹≤ε⇒x≥ε; x⁻¹≥ε⇒x≤ε
; x<y⇒ε<y∙x⁻¹ ; ε<y∙x⁻¹⇒x<y
; x≤y⇒ε≤y∙x⁻¹ ; ε≤y∙x⁻¹⇒x≤y
)
|
