rename preserves-le-xxx

UniMath · Apr 7, 2024 · df3900b · df3900b
1 parent 10279d5
commit df3900b
Show file tree

Hide file tree

Showing 2 changed files with 40 additions and 13 deletions.
diff --git a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md
@@ -226,6 +226,20 @@ module _
       ( is-positive-denominator-fraction-ℤ q)
 ```
 
+### The similarity of integer fractions preserves strict inequality
+
+```agda
+module _
+  (p q p' q' : fraction-ℤ) (H : sim-fraction-ℤ p p') (K : sim-fraction-ℤ q q')
+  where
+
+  preserves-le-sim-fraction-ℤ : le-fraction-ℤ p q → le-fraction-ℤ p' q'
+  preserves-le-sim-fraction-ℤ I =
+    concatenate-sim-le-fraction-ℤ p' p q'
+      ( symmetric-sim-fraction-ℤ p p' H)
+      ( concatenate-le-sim-fraction-ℤ p q q' I K)
+```
+
 ### Fractions with equal denominator compare the same as their numerators
 
 ```agda

diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md
@@ -145,28 +145,41 @@ module _
       ( fraction-ℚ z)
 ```
 
-### Strict inequality on the rational numbers reflects the strict inequality of their underlying fractions
+### The canonical map from integer fractions to the rational numbers preserves strict inequality
 
 ```agda
+module _
+  (p q : fraction-ℤ)
+  where
+
+  preserves-le-rational-fraction-ℤ :
+    le-fraction-ℤ p q → le-ℚ (rational-fraction-ℤ p) (rational-fraction-ℤ q)
+  preserves-le-rational-fraction-ℤ =
+    preserves-le-sim-fraction-ℤ
+      ( p)
+      ( q)
+      ( reduce-fraction-ℤ p)
+      ( reduce-fraction-ℤ q)
+      ( sim-reduced-fraction-ℤ p)
+      ( sim-reduced-fraction-ℤ q)
+
 module _
   (x : ℚ) (p : fraction-ℤ)
   where
 
-  right-le-ℚ-rational-fraction-ℤ-le-fraction-ℤ :
-    le-fraction-ℤ (fraction-ℚ x) p →
-    le-ℚ x (rational-fraction-ℤ p)
-  right-le-ℚ-rational-fraction-ℤ-le-fraction-ℤ H =
+  preserves-le-right-rational-fraction-ℤ :
+    le-fraction-ℤ (fraction-ℚ x) p → le-ℚ x (rational-fraction-ℤ p)
+  preserves-le-right-rational-fraction-ℤ H =
     concatenate-le-sim-fraction-ℤ
       ( fraction-ℚ x)
       ( p)
       ( fraction-ℚ ( rational-fraction-ℤ p))
       ( H)
       ( sim-reduced-fraction-ℤ p)
 
-  left-le-ℚ-rational-fraction-ℤ-le-fraction-ℤ :
-    le-fraction-ℤ p (fraction-ℚ x) →
-    le-ℚ (rational-fraction-ℤ p) x
-  left-le-ℚ-rational-fraction-ℤ-le-fraction-ℤ =
+  preserves-le-left-rational-fraction-ℤ :
+    le-fraction-ℤ p (fraction-ℚ x) → le-ℚ (rational-fraction-ℤ p) x
+  preserves-le-left-rational-fraction-ℤ =
     concatenate-sim-le-fraction-ℤ
       ( fraction-ℚ ( rational-fraction-ℤ p))
       ( p)
@@ -187,7 +200,7 @@ module _
   left-∃-le-ℚ : ∃ ℚ (λ q → le-ℚ q x)
   left-∃-le-ℚ = intro-∃
     ( rational-fraction-ℤ frac)
-    ( left-le-ℚ-rational-fraction-ℤ-le-fraction-ℤ x frac
+    ( preserves-le-left-rational-fraction-ℤ x frac
       ( le-fraction-le-numerator-fraction-ℤ
         ( frac)
         ( fraction-ℚ x)
@@ -200,7 +213,7 @@ module _
   right-∃-le-ℚ : ∃ ℚ (λ r → le-ℚ x r)
   right-∃-le-ℚ = intro-∃
     ( rational-fraction-ℤ frac)
-    ( right-le-ℚ-rational-fraction-ℤ-le-fraction-ℤ x frac
+    ( preserves-le-right-rational-fraction-ℤ x frac
       ( le-fraction-le-numerator-fraction-ℤ
         ( fraction-ℚ x)
         ( frac)
@@ -251,13 +264,13 @@ module _
 
   le-left-mediant-ℚ : le-ℚ x (mediant-ℚ x y)
   le-left-mediant-ℚ =
-    right-le-ℚ-rational-fraction-ℤ-le-fraction-ℤ x
+    preserves-le-right-rational-fraction-ℤ x
       ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
       ( le-left-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H)
 
   le-right-mediant-ℚ : le-ℚ (mediant-ℚ x y) y
   le-right-mediant-ℚ =
-    left-le-ℚ-rational-fraction-ℤ-le-fraction-ℤ y
+    preserves-le-left-rational-fraction-ℤ y
       ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
       ( le-right-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H)
 ```