diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-05 12:08:00 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-05 12:08:00 +0100 |
| commit | 038d2109e78d9c688acfc3338140cc908151db76 (patch) | |
| tree | 3687ed702cf13d728cffe23642a3fe6affb73310 | |
| parent | b212c150ec0a9bf45cf6c28fba997693669e78d2 (diff) | |
Generalise 0 comparison to ≤.
6 files changed, 21 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda index aa37d59..7972c4f 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda @@ -72,4 +72,5 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public ; x⁻¹≤ε⇒x≥ε; x⁻¹≥ε⇒x≤ε ; x<y⇒ε<y∙x⁻¹ ; ε<y∙x⁻¹⇒x<y + ; x≤y⇒ε≤y∙x⁻¹ ; ε≤y∙x⁻¹⇒x≤y ) diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda index 37996b0..6eba0ab 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda @@ -65,6 +65,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public ; -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 + ; x≤y⇒0≤y-x; 0≤y-x⇒x≤y ; 0≤1; 1≈0⇒x≈y; x≉y⇒0<1; x<y⇒0<1 diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda index ab8a37b..c0207a3 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda @@ -78,6 +78,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public ; -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 + ; x≤y⇒0≤y-x; 0≤y-x⇒x≤y ; 0≤1; 1≈0⇒x≈y; x≉y⇒0<1; x<y⇒0<1 diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda index 33578e0..f3ab1c1 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda @@ -75,6 +75,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR ; -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 + ; x≤y⇒0≤y-x; 0≤y-x⇒x≤y ; 0≤1; 1≈0⇒x≈y; x≉y⇒0<1; x<y⇒0<1 diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda index 5cf2d5b..81c57ad 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda @@ -213,3 +213,18 @@ x<y⇒ε<y∙x⁻¹ {x} {y} x<y = begin-strict y ∙ (x ⁻¹ ∙ x) ≈⟨ ∙-congˡ (inverseˡ x) ⟩ y ∙ ε ≈⟨ identityʳ y ⟩ y ∎ + +x≤y⇒ε≤y∙x⁻¹ : ∀ {x y} → x ≤ y → ε ≤ y ∙ x ⁻¹ +x≤y⇒ε≤y∙x⁻¹ {x} {y} x≤y = begin + ε ≈˘⟨ inverseʳ x ⟩ + x ∙ x ⁻¹ ≤⟨ ∙-monoʳ-≤ x≤y ⟩ + y ∙ x ⁻¹ ∎ + +ε≤y∙x⁻¹⇒x≤y : ∀ {x y} → ε ≤ y ∙ x ⁻¹ → x ≤ y +ε≤y∙x⁻¹⇒x≤y {x} {y} ε≤y∙x⁻¹ = begin + x ≈˘⟨ identityˡ x ⟩ + ε ∙ x ≤⟨ ∙-monoʳ-≤ ε≤y∙x⁻¹ ⟩ + y ∙ x ⁻¹ ∙ x ≈⟨ assoc y (x ⁻¹) x ⟩ + y ∙ (x ⁻¹ ∙ x) ≈⟨ ∙-congˡ (inverseˡ x) ⟩ + y ∙ ε ≈⟨ identityʳ y ⟩ + y ∎ diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda index c83f683..5c35176 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda @@ -119,6 +119,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelian ; x<y⇒ε<y∙x⁻¹ to x<y⇒0<y-x ; ε<y∙x⁻¹⇒x<y to 0<y-x⇒x<y + ; x≤y⇒ε≤y∙x⁻¹ to x≤y⇒0≤y-x + ; ε≤y∙x⁻¹⇒x≤y to 0≤y-x⇒x≤y ) -------------------------------------------------------------------------------- |