Apartness in located metric spaces

src/elementary-number-theory/addition-positive-rational-numbers.lagda.md

@@ -226,6 +226,16 @@ module _
     eq-add-split-ℚ⁺
 
   abstract
+    le-left-summand-split-ℚ⁺ : le-ℚ⁺ left-summand-split-ℚ⁺ x
+    le-left-summand-split-ℚ⁺ = le-mediant-zero-ℚ⁺ x
+
+    le-right-summand-split-ℚ⁺ : le-ℚ⁺ right-summand-split-ℚ⁺ x
+    le-right-summand-split-ℚ⁺ =
+      tr
+        ( le-ℚ⁺ right-summand-split-ℚ⁺)
+        ( eq-add-split-ℚ⁺)
+        ( le-right-add-ℚ⁺ left-summand-split-ℚ⁺ right-summand-split-ℚ⁺)
+
     le-add-split-ℚ⁺ :
       (p q r s : ℚ) →
       le-ℚ p (q +ℚ rational-ℚ⁺ left-summand-split-ℚ⁺) →

src/metric-spaces.lagda.md

@@ -56,6 +56,7 @@ metric space, `N d₂ x y` [or](foundation.disjunction.md)
 ```agda
 module metric-spaces where
 
+open import metric-spaces.apartness-located-metric-spaces public
 open import metric-spaces.approximations-located-metric-spaces public
 open import metric-spaces.approximations-metric-spaces public
 open import metric-spaces.bounded-distance-decompositions-of-metric-spaces public

src/metric-spaces/apartness-located-metric-spaces.lagda.md

@@ -0,0 +1,170 @@
+# Apartness in located metric spaces
+
+```agda
+module metric-spaces.apartness-located-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.strict-inequality-positive-rational-numbers
+
+open import foundation.apartness-relations
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.empty-types
+open import foundation.existential-quantification
+open import foundation.negation
+open import foundation.propositional-truncations
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import logic.functoriality-existential-quantification
+
+open import metric-spaces.located-metric-spaces
+```
+
+</details>
+
+## Idea
+
+A [located metric space](metric-spaces.located-metric-spaces.md) `M` induces an
+[apartness relation](foundation.apartness-relations.md) `#` such that `x # y` if
+there [exists](foundation.existential-quantification.md) an `ε : ℚ⁺` such that
+`x` and `y` are [not](foundation.negation.md) in an `ε`-neighborhood of each
+other.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (M : Located-Metric-Space l1 l2)
+  where
+
+  apart-prop-Located-Metric-Space :
+    Relation-Prop l2 (type-Located-Metric-Space M)
+  apart-prop-Located-Metric-Space x y =
+    ∃ ℚ⁺ (λ ε → ¬' (neighborhood-prop-Located-Metric-Space M ε x y))
+
+  apart-Located-Metric-Space : Relation l2 (type-Located-Metric-Space M)
+  apart-Located-Metric-Space =
+    type-Relation-Prop apart-prop-Located-Metric-Space
+```
+
+## Properties
+
+### The apartness relation of a located metric space is antireflexive
+
+```agda
+module _
+  {l1 l2 : Level} (M : Located-Metric-Space l1 l2)
+  where
+
+  abstract
+    is-antireflexive-apart-Located-Metric-Space :
+      is-antireflexive (apart-prop-Located-Metric-Space M)
+    is-antireflexive-apart-Located-Metric-Space x =
+      elim-exists
+        ( empty-Prop)
+        ( λ ε ¬Nεxx → ¬Nεxx (refl-neighborhood-Located-Metric-Space M ε x))
+```
+
+### The apartness relation of a located metric space is symmetric
+
+```agda
+module _
+  {l1 l2 : Level} (M : Located-Metric-Space l1 l2)
+  where
+
+  abstract
+    is-symmetric-apart-Located-Metric-Space :
+      is-symmetric (apart-Located-Metric-Space M)
+    is-symmetric-apart-Located-Metric-Space x y =
+      map-tot-exists
+        ( λ ε ¬Nεxy Nεyx →
+          ¬Nεxy (symmetric-neighborhood-Located-Metric-Space M ε y x Nεyx))
+```
+
+### The apartness relation of a located metric space is cotransitive
+
+```agda
+module _
+  {l1 l2 : Level} (M : Located-Metric-Space l1 l2)
+  where
+
+  abstract
+    is-cotransitive-apart-Located-Metric-Space :
+      is-cotransitive (apart-prop-Located-Metric-Space M)
+    is-cotransitive-apart-Located-Metric-Space x y z x#y =
+      let
+        motive =
+          apart-prop-Located-Metric-Space M x z ∨
+          apart-prop-Located-Metric-Space M y z
+        open do-syntax-trunc-Prop motive
+      in do
+        (dxy , ¬Ndxy) ← x#y
+        let (δ , ε , δ+ε=dxy) = split-ℚ⁺ dxy
+        elim-disjunction
+          ( motive)
+          ( λ ¬Nδ'xz →
+            inl-disjunction (intro-exists (mediant-zero-ℚ⁺ δ) ¬Nδ'xz))
+          ( λ Nδxz →
+            elim-disjunction
+              ( motive)
+              ( λ ¬Nε'yz →
+                inr-disjunction (intro-exists (mediant-zero-ℚ⁺ ε) ¬Nε'yz))
+              ( λ Nεyz →
+                ex-falso
+                  ( ¬Ndxy
+                    ( tr
+                      ( λ d → neighborhood-Located-Metric-Space M d x y)
+                      ( δ+ε=dxy)
+                      ( triangular-neighborhood-Located-Metric-Space M
+                        ( x)
+                        ( z)
+                        ( y)
+                        ( δ)
+                        ( ε)
+                        ( symmetric-neighborhood-Located-Metric-Space M
+                          ( ε)
+                          ( y)
+                          ( z)
+                          ( Nεyz))
+                        ( Nδxz)))))
+              ( is-located-Located-Metric-Space M
+                ( y)
+                ( z)
+                ( mediant-zero-ℚ⁺ ε)
+                ( ε)
+                ( le-mediant-zero-ℚ⁺ ε)))
+          ( is-located-Located-Metric-Space M
+            ( x)
+            ( z)
+            ( mediant-zero-ℚ⁺ δ)
+            ( δ)
+            ( le-mediant-zero-ℚ⁺ δ))
+```
+
+### The apartness relation on located metric spaces is an apartness relation
+
+```agda
+module _
+  {l1 l2 : Level} (M : Located-Metric-Space l1 l2)
+  where
+
+  is-apartness-relation-apart-Located-Metric-Space :
+    is-apartness-relation (apart-prop-Located-Metric-Space M)
+  is-apartness-relation-apart-Located-Metric-Space =
+    ( is-antireflexive-apart-Located-Metric-Space M ,
+      is-symmetric-apart-Located-Metric-Space M ,
+      is-cotransitive-apart-Located-Metric-Space M)
+
+  apartness-relation-Located-Metric-Space :
+    Apartness-Relation l2 (type-Located-Metric-Space M)
+  apartness-relation-Located-Metric-Space =
+    ( apart-prop-Located-Metric-Space M ,
+      is-apartness-relation-apart-Located-Metric-Space)
+```

src/metric-spaces/located-metric-spaces.lagda.md

@@ -7,12 +7,14 @@ module metric-spaces.located-metric-spaces where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-positive-rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
+open import foundation.binary-relations
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.disjunction
@@ -101,9 +103,39 @@ module _
   type-Located-Metric-Space =
     type-Metric-Space metric-space-Located-Metric-Space
 
-  is-located-metric-space-Located-Metric-Space :
+  neighborhood-prop-Located-Metric-Space :
+    ℚ⁺ → Relation-Prop l2 type-Located-Metric-Space
+  neighborhood-prop-Located-Metric-Space =
+    neighborhood-prop-Metric-Space metric-space-Located-Metric-Space
+
+  neighborhood-Located-Metric-Space : ℚ⁺ → Relation l2 type-Located-Metric-Space
+  neighborhood-Located-Metric-Space =
+    neighborhood-Metric-Space metric-space-Located-Metric-Space
+
+  refl-neighborhood-Located-Metric-Space :
+    (d : ℚ⁺) (x : type-Located-Metric-Space) →
+    neighborhood-Located-Metric-Space d x x
+  refl-neighborhood-Located-Metric-Space =
+    refl-neighborhood-Metric-Space metric-space-Located-Metric-Space
+
+  symmetric-neighborhood-Located-Metric-Space :
+    (d : ℚ⁺) (x y : type-Located-Metric-Space) →
+    neighborhood-Located-Metric-Space d x y →
+    neighborhood-Located-Metric-Space d y x
+  symmetric-neighborhood-Located-Metric-Space =
+    symmetric-neighborhood-Metric-Space metric-space-Located-Metric-Space
+
+  triangular-neighborhood-Located-Metric-Space :
+    (x y z : type-Located-Metric-Space) (d₁ d₂ : ℚ⁺) →
+    neighborhood-Located-Metric-Space d₂ y z →
+    neighborhood-Located-Metric-Space d₁ x y →
+    neighborhood-Located-Metric-Space (d₁ +ℚ⁺ d₂) x z
+  triangular-neighborhood-Located-Metric-Space =
+    triangular-neighborhood-Metric-Space metric-space-Located-Metric-Space
+
+  is-located-Located-Metric-Space :
     is-located-Metric-Space metric-space-Located-Metric-Space
-  is-located-metric-space-Located-Metric-Space = pr2 X
+  is-located-Located-Metric-Space = pr2 X
 
   set-Located-Metric-Space : Set l1
   set-Located-Metric-Space = set-Metric-Space metric-space-Located-Metric-Space

src/metric-spaces/metrics-of-metric-spaces.lagda.md

@@ -11,6 +11,7 @@ open import elementary-number-theory.positive-rational-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.equivalences
+open import foundation.functoriality-disjunction
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.propositional-truncations
@@ -20,12 +21,15 @@ open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import metric-spaces.equality-of-metric-spaces
+open import metric-spaces.located-metric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.metrics
 
 open import real-numbers.addition-nonnegative-real-numbers
+open import real-numbers.dedekind-real-numbers
 open import real-numbers.inequality-nonnegative-real-numbers
 open import real-numbers.nonnegative-real-numbers
+open import real-numbers.rational-real-numbers
 open import real-numbers.saturation-inequality-nonnegative-real-numbers
 open import real-numbers.similarity-nonnegative-real-numbers
 open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers
@@ -211,6 +215,37 @@ module _
   isometric-equiv-metric-is-metric-of-Metric-Space = (id-equiv , is-metric-M-ρ)
 ```
 
+### If `ρ` is a metric for a metric space `M`, then `M` is located
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  (ρ : distance-function l2 (set-Metric-Space M))
+  (is-metric-M-ρ : is-metric-of-Metric-Space M ρ)
+  where
+
+  abstract
+    is-located-is-metric-of-Metric-Space : is-located-Metric-Space M
+    is-located-is-metric-of-Metric-Space x y δ ε δ<ε =
+      map-disjunction
+        ( λ δ<ρxy Nδxy →
+          not-le-leq-ℝ
+            ( real-ℝ⁰⁺ (ρ x y))
+            ( real-ℚ⁺ δ)
+            ( forward-implication (is-metric-M-ρ δ x y) Nδxy)
+            ( le-real-is-in-lower-cut-ℚ
+              ( real-ℝ⁰⁺ (ρ x y))
+              ( δ<ρxy)))
+        ( λ ρxy<ε →
+          backward-implication
+            ( is-metric-M-ρ ε x y)
+            ( leq-le-ℝ
+              ( le-real-is-in-upper-cut-ℚ
+                ( real-ℝ⁰⁺ (ρ x y))
+                ( ρxy<ε))))
+        ( is-located-lower-upper-cut-ℝ (real-ℝ⁰⁺ (ρ x y)) δ<ε)
+```
+
 ### If `ρ` is a metric for a metric space `M` at the appropriate universe level, then `M` is equal to the metric space induced by `ρ`
 
 ```agda

src/real-numbers.lagda.md

@@ -43,6 +43,7 @@ open import real-numbers.large-multiplicative-monoid-of-real-numbers public
 open import real-numbers.large-ring-of-real-numbers public
 open import real-numbers.limits-sequences-real-numbers public
 open import real-numbers.lipschitz-continuity-multiplication-real-numbers public
+open import real-numbers.located-metric-space-of-real-numbers public
 open import real-numbers.lower-dedekind-real-numbers public
 open import real-numbers.maximum-finite-families-real-numbers public
 open import real-numbers.maximum-inhabited-finitely-enumerable-subsets-real-numbers public

src/real-numbers/absolute-value-real-numbers.lagda.md

@@ -27,13 +27,15 @@ open import metric-spaces.short-functions-metric-spaces
 open import real-numbers.addition-real-numbers
 open import real-numbers.binary-maximum-real-numbers
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.difference-real-numbers
 open import real-numbers.inequalities-addition-and-subtraction-real-numbers
 open import real-numbers.inequality-real-numbers
 open import real-numbers.isometry-negation-real-numbers
 open import real-numbers.metric-space-of-real-numbers
 open import real-numbers.multiplication-nonnegative-real-numbers
 open import real-numbers.multiplication-real-numbers
 open import real-numbers.negation-real-numbers
+open import real-numbers.negative-real-numbers
 open import real-numbers.nonnegative-real-numbers
 open import real-numbers.positive-and-negative-real-numbers
 open import real-numbers.positive-real-numbers
@@ -42,6 +44,7 @@ open import real-numbers.saturation-inequality-real-numbers
 open import real-numbers.similarity-real-numbers
 open import real-numbers.square-roots-nonnegative-real-numbers
 open import real-numbers.squares-real-numbers
+open import real-numbers.strict-inequality-real-numbers
 ```
 
 </details>
@@ -132,11 +135,24 @@ abstract opaque
           ( x)
           ( 0≤x)
           ( tr (leq-ℝ (neg-ℝ x)) neg-zero-ℝ (neg-leq-ℝ 0≤x))))
+```
+
+### The absolute value of a positive real number is itself
 
+```agda
+abstract
   abs-real-ℝ⁺ : {l : Level} (x : ℝ⁺ l) → abs-ℝ (real-ℝ⁺ x) ＝ real-ℝ⁺ x
   abs-real-ℝ⁺ x = abs-real-ℝ⁰⁺ (nonnegative-ℝ⁺ x)
 ```
 
+### The absolute value of a negative real number is its negation
+
+```agda
+abstract
+  abs-real-ℝ⁻ : {l : Level} (x : ℝ⁻ l) → abs-ℝ (real-ℝ⁻ x) ＝ neg-ℝ (real-ℝ⁻ x)
+  abs-real-ℝ⁻ x⁻@(x , _) = inv (abs-neg-ℝ x) ∙ abs-real-ℝ⁺ (neg-ℝ⁻ x⁻)
+```
+
 ### `x` is between `-|x|` and `|x|`
 
 ```agda
@@ -402,3 +418,17 @@ abstract
       ＝ abs-ℝ x *ℝ abs-ℝ y
         by inv (ap-mul-ℝ (eq-abs-sqrt-square-ℝ x) (eq-abs-sqrt-square-ℝ y))
 ```
+
+### For any `ε : ℚ⁺`, `(abs-ℝ x - ε < x) ∨ (abs-ℝ x - ε < -x)`
+
+```agda
+abstract opaque
+  unfolding abs-ℝ
+
+  approximate-below-abs-ℝ :
+    {l : Level} (x : ℝ l) (ε : ℚ⁺) →
+    disjunction-type
+      ( le-ℝ (abs-ℝ x -ℝ real-ℚ⁺ ε) x)
+      ( le-ℝ (abs-ℝ x -ℝ real-ℚ⁺ ε) (neg-ℝ x))
+  approximate-below-abs-ℝ x = approximate-below-max-ℝ x (neg-ℝ x)
+```