Multiplication of interior intervals in the rational numbers

src/elementary-number-theory.lagda.md

@@ -40,6 +40,7 @@ open import elementary-number-theory.binomial-theorem-integers public
 open import elementary-number-theory.binomial-theorem-natural-numbers public
 open import elementary-number-theory.bounded-sums-arithmetic-functions public
 open import elementary-number-theory.catalan-numbers public
+open import elementary-number-theory.closed-interval-preserving-maps-rational-numbers public
 open import elementary-number-theory.closed-intervals-rational-numbers public
 open import elementary-number-theory.cofibonacci public
 open import elementary-number-theory.collatz-bijection public
@@ -107,6 +108,7 @@ open import elementary-number-theory.initial-segments-natural-numbers public
 open import elementary-number-theory.integer-fractions public
 open import elementary-number-theory.integer-partitions public
 open import elementary-number-theory.integers public
+open import elementary-number-theory.interior-closed-intervals-rational-numbers public
 open import elementary-number-theory.intersections-closed-intervals-rational-numbers public
 open import elementary-number-theory.jacobi-symbol public
 open import elementary-number-theory.kolakoski-sequence public
@@ -118,6 +120,7 @@ open import elementary-number-theory.maximum-rational-numbers public
 open import elementary-number-theory.maximum-standard-finite-types public
 open import elementary-number-theory.mediant-integer-fractions public
 open import elementary-number-theory.mersenne-primes public
+open import elementary-number-theory.minima-and-maxima-rational-numbers public
 open import elementary-number-theory.minimum-natural-numbers public
 open import elementary-number-theory.minimum-positive-rational-numbers public
 open import elementary-number-theory.minimum-rational-numbers public
@@ -129,10 +132,13 @@ open import elementary-number-theory.monoid-of-natural-numbers-with-maximum publ
 open import elementary-number-theory.multiplication-closed-intervals-rational-numbers public
 open import elementary-number-theory.multiplication-integer-fractions public
 open import elementary-number-theory.multiplication-integers public
+open import elementary-number-theory.multiplication-interior-closed-intervals-rational-numbers public
 open import elementary-number-theory.multiplication-lists-of-natural-numbers public
 open import elementary-number-theory.multiplication-natural-numbers public
 open import elementary-number-theory.multiplication-nonnegative-rational-numbers public
+open import elementary-number-theory.multiplication-nonpositive-rational-numbers public
 open import elementary-number-theory.multiplication-positive-and-negative-integers public
+open import elementary-number-theory.multiplication-positive-and-negative-rational-numbers public
 open import elementary-number-theory.multiplication-positive-rational-numbers public
 open import elementary-number-theory.multiplication-rational-numbers public
 open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers public
@@ -144,13 +150,15 @@ open import elementary-number-theory.multiplicative-units-integers public
 open import elementary-number-theory.multiplicative-units-standard-cyclic-rings public
 open import elementary-number-theory.multiset-coefficients public
 open import elementary-number-theory.natural-numbers public
+open import elementary-number-theory.negation-closed-intervals-rational-numbers public
 open import elementary-number-theory.negative-integer-fractions public
 open import elementary-number-theory.negative-integers public
 open import elementary-number-theory.negative-rational-numbers public
 open import elementary-number-theory.nonnegative-integer-fractions public
 open import elementary-number-theory.nonnegative-integers public
 open import elementary-number-theory.nonnegative-rational-numbers public
 open import elementary-number-theory.nonpositive-integers public
+open import elementary-number-theory.nonpositive-rational-numbers public
 open import elementary-number-theory.nonzero-integers public
 open import elementary-number-theory.nonzero-natural-numbers public
 open import elementary-number-theory.nonzero-rational-numbers public
@@ -170,6 +178,7 @@ open import elementary-number-theory.powers-integers public
 open import elementary-number-theory.powers-of-two public
 open import elementary-number-theory.prime-numbers public
 open import elementary-number-theory.products-of-natural-numbers public
+open import elementary-number-theory.proper-closed-intervals-rational-numbers public
 open import elementary-number-theory.proper-divisors-natural-numbers public
 open import elementary-number-theory.pythagorean-triples public
 open import elementary-number-theory.rational-numbers public

src/elementary-number-theory/closed-interval-preserving-maps-rational-numbers.lagda.md

@@ -0,0 +1,46 @@
+# Closed interval preserving endomaps on the rational numbers
+
+```agda
+module elementary-number-theory.closed-interval-preserving-maps-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.closed-intervals-rational-numbers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import order-theory.closed-interval-preserving-maps-posets
+```
+
+</details>
+
+## Idea
+
+A map from the [rational numbers](elementary-number-theory.rational-numbers.md)
+to themselves `f : ℚ → ℚ` is
+{{#concept "closed interval preserving" Agda=is-closed-interval-map-ℚ disambiguation="map between rational numbers"}}
+if the [image](foundation.images-subtypes.md) of a
+[closed interval](elementary-number-theory.closed-intervals-rational-numbers.md)
+is always a closed interval in `Y`. Equivalently, it is a
+[closed interval preserving map](order-theory.closed-interval-preserving-maps-total-orders.md)
+on the
+[total order of rational numbers](elementary-number-theory.decidable-total-order-rational-numbers.md).
+
+## Definition
+
+```agda
+is-closed-interval-map-ℚ :
+  (ℚ → ℚ) → ([a,b] [c,d] : closed-interval-ℚ) → UU lzero
+is-closed-interval-map-ℚ = is-closed-interval-map-Poset ℚ-Poset ℚ-Poset
+
+is-closed-interval-map-prop-ℚ :
+  (ℚ → ℚ) → closed-interval-ℚ → closed-interval-ℚ →
+  Prop lzero
+is-closed-interval-map-prop-ℚ =
+  is-closed-interval-map-prop-Poset ℚ-Poset ℚ-Poset
+```

src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md

@@ -59,7 +59,13 @@ lower-bound-closed-interval-ℚ =
 upper-bound-closed-interval-ℚ : closed-interval-ℚ → ℚ
 upper-bound-closed-interval-ℚ =
   upper-bound-closed-interval-Poset ℚ-Poset
+```
+
+## Properties
 
+### The subtype associated with a closed interval
+
+```agda
 subtype-closed-interval-ℚ :
   closed-interval-ℚ → subtype lzero ℚ
 subtype-closed-interval-ℚ =
@@ -68,21 +74,23 @@ subtype-closed-interval-ℚ =
 is-in-closed-interval-ℚ : closed-interval-ℚ → ℚ → UU lzero
 is-in-closed-interval-ℚ [a,b] =
   is-in-subtype (subtype-closed-interval-ℚ [a,b])
+```
 
-is-closed-interval-map-prop-ℚ :
-  (ℚ → ℚ) → closed-interval-ℚ → closed-interval-ℚ →
-  Prop lzero
-is-closed-interval-map-prop-ℚ =
-  is-closed-interval-map-prop-Poset ℚ-Poset ℚ-Poset
+### The property of being above or below a closed interval
 
+```agda
 is-below-prop-closed-interval-ℚ :
   closed-interval-ℚ → subtype lzero ℚ
 is-below-prop-closed-interval-ℚ ((a , _) , _) b = le-ℚ-Prop b a
 
 is-above-prop-closed-interval-ℚ :
   closed-interval-ℚ → subtype lzero ℚ
 is-above-prop-closed-interval-ℚ ((_ , a) , _) b = le-ℚ-Prop a b
+```
+
+### The width of a closed interval
 
+```agda
 nonnegative-width-closed-interval-ℚ :
   closed-interval-ℚ → ℚ⁰⁺
 nonnegative-width-closed-interval-ℚ ((a , b) , a≤b) =
@@ -91,11 +99,6 @@ nonnegative-width-closed-interval-ℚ ((a , b) , a≤b) =
 width-closed-interval-ℚ : closed-interval-ℚ → ℚ
 width-closed-interval-ℚ [a,b] =
   rational-ℚ⁰⁺ (nonnegative-width-closed-interval-ℚ [a,b])
-
-is-injective-subtype-closed-interval-ℚ :
-  is-injective subtype-closed-interval-ℚ
-is-injective-subtype-closed-interval-ℚ =
-  is-injective-subtype-closed-interval-Poset ℚ-Poset
 ```
 
 ### Important ranges
@@ -108,7 +111,14 @@ one-one-closed-interval-ℚ : closed-interval-ℚ
 one-one-closed-interval-ℚ = ((one-ℚ , one-ℚ) , refl-leq-ℚ one-ℚ)
 ```
 
-## Properties
+### The map from closed intervals to their subtypes is injective
+
+```agda
+is-injective-subtype-closed-interval-ℚ :
+  is-injective subtype-closed-interval-ℚ
+is-injective-subtype-closed-interval-ℚ =
+  is-injective-subtype-closed-interval-Poset ℚ-Poset
+```
 
 ### Characterization of equality
 
@@ -152,10 +162,18 @@ abstract
       ( right-leq-left-max-ℚ p q q≤p)
 ```
 
-### Maps from rational intervals to rational intervals
+### The bounds of a closed interval are elements
 
 ```agda
-is-closed-interval-map-ℚ :
-  (ℚ → ℚ) → ([a,b] [c,d] : closed-interval-ℚ) → UU lzero
-is-closed-interval-map-ℚ = is-closed-interval-map-Poset ℚ-Poset ℚ-Poset
+lower-bound-is-in-closed-interval-ℚ :
+  ([a,b] : closed-interval-ℚ) →
+  is-in-closed-interval-ℚ [a,b] (lower-bound-closed-interval-ℚ [a,b])
+lower-bound-is-in-closed-interval-ℚ =
+  lower-bound-is-in-closed-interval-Poset ℚ-Poset
+
+upper-bound-is-in-closed-interval-ℚ :
+  ([a,b] : closed-interval-ℚ) →
+  is-in-closed-interval-ℚ [a,b] (upper-bound-closed-interval-ℚ [a,b])
+upper-bound-is-in-closed-interval-ℚ =
+  upper-bound-is-in-closed-interval-Poset ℚ-Poset
 ```

src/elementary-number-theory/interior-closed-intervals-rational-numbers.lagda.md

@@ -0,0 +1,40 @@
+# Interior closed intervals in the rational numbers
+
+```agda
+module elementary-number-theory.interior-closed-intervals-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.closed-intervals-rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given two
+[closed intervals of rational numbers](elementary-number-theory.closed-intervals-rational-numbers.md)
+[a, b] and [c, d], then [c, d] is said to be
+{{#concept "interior" Disambiguation="closed intervals of rational numbers" Agda=is-interior-closed-interval-ℚ}}
+to [a, b] if `a < c` and `d < b`.
+
+## Definition
+
+```agda
+is-interior-prop-closed-interval-ℚ :
+  closed-interval-ℚ → closed-interval-ℚ → Prop lzero
+is-interior-prop-closed-interval-ℚ ((x , y) , _) ((x' , y') , _) =
+  le-ℚ-Prop x x' ∧ le-ℚ-Prop y' y
+
+is-interior-closed-interval-ℚ : closed-interval-ℚ → closed-interval-ℚ → UU lzero
+is-interior-closed-interval-ℚ [x,y] [x',y'] =
+  type-Prop (is-interior-prop-closed-interval-ℚ [x,y] [x',y'])
+```

src/elementary-number-theory/minima-and-maxima-rational-numbers.lagda.md

@@ -0,0 +1,69 @@
+# Minima and maxima on the rational numbers
+
+```agda
+module elementary-number-theory.minima-and-maxima-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.maximum-rational-numbers
+open import elementary-number-theory.minimum-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
+open import foundation.identity-types
+```
+
+</details>
+
+## Idea
+
+On this page, we outline basic relations between
+[minima](elementary-number-theory.minimum-rational-numbers.md) and
+[maxima](elementary-number-theory.maximum-rational-numbers.md) of
+[rational numbers](elementary-number-theory.rational-numbers.md).
+
+## Lemmas
+
+### The negation of the minimum of rational numbers is the maximum of the negations
+
+```agda
+module _
+  (p q : ℚ)
+  where
+
+  abstract
+    neg-min-ℚ : neg-ℚ (min-ℚ p q) ＝ max-ℚ (neg-ℚ p) (neg-ℚ q)
+    neg-min-ℚ =
+      rec-coproduct
+        ( λ p≤q →
+          ( ap neg-ℚ (left-leq-right-min-ℚ p q p≤q)) ∙
+          ( inv (right-leq-left-max-ℚ _ _ (neg-leq-ℚ _ _ p≤q))))
+        ( λ q≤p →
+          ( ap neg-ℚ (right-leq-left-min-ℚ p q q≤p)) ∙
+          ( inv (left-leq-right-max-ℚ _ _ (neg-leq-ℚ _ _ q≤p))))
+        ( linear-leq-ℚ p q)
+```
+
+### The negation of the maximum of rational numbers is the minimum of the negations
+
+```agda
+module _
+  (p q : ℚ)
+  where
+
+  abstract
+    neg-max-ℚ : neg-ℚ (max-ℚ p q) ＝ min-ℚ (neg-ℚ p) (neg-ℚ q)
+    neg-max-ℚ =
+      rec-coproduct
+        ( λ p≤q →
+          ( ap neg-ℚ (left-leq-right-max-ℚ _ _ p≤q)) ∙
+          ( inv (right-leq-left-min-ℚ _ _ (neg-leq-ℚ _ _ p≤q))))
+        ( λ q≤p →
+          ( ap neg-ℚ (right-leq-left-max-ℚ _ _ q≤p)) ∙
+          ( inv (left-leq-right-min-ℚ _ _ (neg-leq-ℚ _ _ q≤p))))
+        ( linear-leq-ℚ p q)
+```