The image of a totally bounded metric space under a uniformly continuous function is totally bounded (#1513)

Author: lowasser

src/foundation/images-subtypes.lagda.md

@@ -78,6 +78,9 @@ module _
   im-subtype : subtype (l1 ⊔ l2 ⊔ l3) B
   im-subtype y = subtype-im (f ∘ inclusion-subtype S) y
 
+  type-im-subtype : UU (l1 ⊔ l2 ⊔ l3)
+  type-im-subtype = type-subtype im-subtype
+
   is-in-im-subtype : B → UU (l1 ⊔ l2 ⊔ l3)
   is-in-im-subtype = is-in-subtype im-subtype
 ```

src/foundation/images.lagda.md

@@ -7,22 +7,28 @@ module foundation.images where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.embeddings
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.propositional-truncations
+open import foundation.retractions
+open import foundation.sections
 open import foundation.slice
 open import foundation.subtype-identity-principle
 open import foundation.surjective-maps
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.1-types
 open import foundation-core.commuting-triangles-of-maps
-open import foundation-core.embeddings
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
+open import foundation-core.propositional-maps
 open import foundation-core.propositions
 open import foundation-core.sets
 open import foundation-core.subtypes
@@ -218,6 +224,31 @@ im-1-Type :
 im-1-Type X f = im-Truncated-Type zero-𝕋 X f
 ```
 
+### The unit map of the image of an embedding is an equivalence
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A ↪ B)
+  where
+
+  map-unit-im-emb : A → im (map-emb f)
+  map-unit-im-emb = map-unit-im (map-emb f)
+
+  abstract
+    is-equiv-unit-im-emb : is-equiv map-unit-im-emb
+    is-equiv-unit-im-emb =
+      is-equiv-is-emb-is-surjective
+        ( is-surjective-map-unit-im (map-emb f))
+        ( is-emb-right-factor
+          ( inclusion-im (map-emb f))
+          ( map-unit-im (map-emb f))
+          ( is-emb-inclusion-im (map-emb f))
+          ( is-emb-map-emb f))
+
+  equiv-im-emb : A ≃ im (map-emb f)
+  equiv-im-emb = (map-unit-im-emb , is-equiv-unit-im-emb)
+```
+
 ## External links
 
 - [Image (mathematics)](<https://en.wikipedia.org/wiki/Image_(mathematics)>) at

src/foundation/surjective-maps.lagda.md

@@ -13,6 +13,7 @@ open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.diagonal-maps-of-types
 open import foundation.embeddings
+open import foundation.empty-types
 open import foundation.equality-cartesian-product-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-propositional-truncation
@@ -237,6 +238,16 @@ surjection-retract R =
   ( map-retraction-retract R , is-surjective-has-section (section-retract R))
 ```
 
+### If an empty type has a surjection into another type, that type is empty
+
+```agda
+abstract
+  is-empty-surjection :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} → A ↠ B → is-empty A → is-empty B
+  is-empty-surjection A↠B ¬A b =
+    rec-trunc-Prop empty-Prop (¬A ∘ pr1) (is-surjective-map-surjection A↠B b)
+```
+
 ### Any split surjective map is surjective
 
 ```agda

src/metric-spaces.lagda.md

@@ -74,6 +74,10 @@ open import metric-spaces.functions-metric-spaces public
 open import metric-spaces.functions-pseudometric-spaces public
 open import metric-spaces.functor-category-set-functions-isometry-metric-spaces public
 open import metric-spaces.functor-category-short-isometry-metric-spaces public
+open import metric-spaces.images-isometries-metric-spaces public
+open import metric-spaces.images-metric-spaces public
+open import metric-spaces.images-short-functions-metric-spaces public
+open import metric-spaces.images-uniformly-continuous-functions-metric-spaces public
 open import metric-spaces.indexed-sums-metric-spaces public
 open import metric-spaces.interior-subsets-metric-spaces public
 open import metric-spaces.isometries-metric-spaces public

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

@@ -10,15 +10,30 @@ module metric-spaces.approximations-metric-spaces where
 open import elementary-number-theory.positive-rational-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.existential-quantification
 open import foundation.full-subtypes
+open import foundation.function-types
+open import foundation.images
+open import foundation.images-subtypes
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.subtypes
+open import foundation.transport-along-identifications
 open import foundation.unions-subtypes
 open import foundation.universe-levels
 
-open import metric-spaces.located-metric-spaces
+open import metric-spaces.equality-of-metric-spaces
+open import metric-spaces.functions-metric-spaces
+open import metric-spaces.images-isometries-metric-spaces
+open import metric-spaces.images-metric-spaces
+open import metric-spaces.images-short-functions-metric-spaces
+open import metric-spaces.images-uniformly-continuous-functions-metric-spaces
+open import metric-spaces.isometries-metric-spaces
 open import metric-spaces.metric-spaces
+open import metric-spaces.short-functions-metric-spaces
 open import metric-spaces.subspaces-metric-spaces
+open import metric-spaces.uniformly-continuous-functions-metric-spaces
 ```
 
 </details>
@@ -72,6 +87,155 @@ module _
   type-approximation-Metric-Space : UU (l1 ⊔ l3)
   type-approximation-Metric-Space =
     type-subtype subset-approximation-Metric-Space
+
+  is-approximation-approximation-Metric-Space :
+    is-approximation-Metric-Space X ε subset-approximation-Metric-Space
+  is-approximation-approximation-Metric-Space = pr2 S
+```
+
+## Properties
+
+### If `μ` is a modulus of uniform continuity for `f : X → Y` and `A` is a `(μ ε)`-approximation of `X`, then `im f A` is an `ε`-approximation of `im f X`
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
+  (f : type-function-Metric-Space X Y) {μ : ℚ⁺ → ℚ⁺}
+  (is-modulus-ucont-f-μ :
+    is-modulus-of-uniform-continuity-function-Metric-Space X Y f μ)
+  (ε : ℚ⁺) (A : approximation-Metric-Space l5 X (μ ε))
+  where
+
+  abstract
+    is-approximation-im-uniformly-continuous-function-approximation-Metric-Space :
+      is-approximation-Metric-Space
+        ( im-Metric-Space X Y f)
+        ( ε)
+        ( im-subtype
+          ( map-unit-im f)
+          ( subset-approximation-Metric-Space X (μ ε) A))
+    is-approximation-im-uniformly-continuous-function-approximation-Metric-Space
+      (y , ∃x:fx=y) =
+        let
+          open
+            do-syntax-trunc-Prop
+              ( ∃ _ (λ z → neighborhood-prop-Metric-Space Y ε (pr1 (pr1 z)) y))
+        in do
+          (x , fx=y) ← ∃x:fx=y
+          ((a , a∈A) , Nμεax) ←
+            is-approximation-approximation-Metric-Space X (μ ε) A x
+          intro-exists
+            ( map-unit-im
+              ( map-unit-im f ∘
+                inclusion-subtype
+                  ( subset-approximation-Metric-Space X (μ ε) A))
+              ( a , a∈A))
+            ( tr
+              ( neighborhood-Metric-Space Y ε (f a))
+              ( fx=y)
+              ( is-modulus-ucont-f-μ a ε x Nμεax))
+
+  approximation-im-uniformly-continuous-function-approximation-Metric-Space :
+    approximation-Metric-Space (l1 ⊔ l3 ⊔ l5) (im-Metric-Space X Y f) ε
+  approximation-im-uniformly-continuous-function-approximation-Metric-Space =
+    ( im-subtype (map-unit-im f) (subset-approximation-Metric-Space X (μ ε) A) ,
+      is-approximation-im-uniformly-continuous-function-approximation-Metric-Space)
+```
+
+### If `f : X → Y` is a short function and `A` is an `ε`-approximation of `X`, then `im f A` is an `ε`-approximation of `im f X`
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
+  (f : short-function-Metric-Space X Y)
+  (ε : ℚ⁺) (A : approximation-Metric-Space l5 X ε)
+  where
+
+  approximation-im-short-function-approximation-Metric-Space :
+    approximation-Metric-Space
+      ( l1 ⊔ l3 ⊔ l5)
+      ( im-short-function-Metric-Space X Y f)
+      ( ε)
+  approximation-im-short-function-approximation-Metric-Space =
+    approximation-im-uniformly-continuous-function-approximation-Metric-Space
+      ( X)
+      ( Y)
+      ( map-short-function-Metric-Space X Y f)
+      ( id-is-modulus-of-uniform-continuity-is-short-function-Metric-Space
+        ( X)
+        ( Y)
+        ( map-short-function-Metric-Space X Y f)
+        ( is-short-map-short-function-Metric-Space X Y f))
+      ( ε)
+      ( A)
+```
+
+### If `f : X → Y` is an isometry and `A` is an `ε`-approximation of `X`, then `im f A` is an `ε`-approximation of `im f X`
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
+  (f : isometry-Metric-Space X Y)
+  (ε : ℚ⁺) (A : approximation-Metric-Space l5 X ε)
+  where
+
+  approximation-im-isometry-approximation-Metric-Space :
+    approximation-Metric-Space
+      ( l1 ⊔ l3 ⊔ l5)
+      ( im-isometry-Metric-Space X Y f)
+      ( ε)
+  approximation-im-isometry-approximation-Metric-Space =
+    approximation-im-short-function-approximation-Metric-Space X Y
+      ( short-isometry-Metric-Space X Y f)
+      ( ε)
+      ( A)
+```
+
+### If `f : X ≃ Y` is an isometric equivalence and `A` is an `ε`-approximation of `X`, then `im f A` is an `ε`-approximation of `Y`
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
+  (f : isometric-equiv-Metric-Space X Y)
+  (ε : ℚ⁺) (A : approximation-Metric-Space l5 X ε)
+  where
+
+  abstract
+    is-approximation-im-isometric-equiv-approximation-Metric-Space :
+      is-approximation-Metric-Space
+        ( Y)
+        ( ε)
+        ( im-subtype
+          ( map-isometric-equiv-Metric-Space X Y f)
+          ( subset-approximation-Metric-Space X ε A))
+    is-approximation-im-isometric-equiv-approximation-Metric-Space y =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( ∃ _ (λ z → neighborhood-prop-Metric-Space Y ε (pr1 z) y))
+      in do
+        let x = map-inv-isometric-equiv-Metric-Space X Y f y
+        ((a , a∈A) , Nεax) ← is-approximation-approximation-Metric-Space X ε A x
+        intro-exists
+          ( map-unit-im
+            ( map-isometric-equiv-Metric-Space X Y f ∘
+              inclusion-subtype (subset-approximation-Metric-Space X ε A))
+            ( a , a∈A))
+          ( tr
+            ( neighborhood-Metric-Space Y ε
+              ( map-isometric-equiv-Metric-Space X Y f a))
+            ( is-section-map-inv-isometric-equiv-Metric-Space X Y f y)
+            ( forward-implication
+              ( is-isometry-map-isometric-equiv-Metric-Space X Y f ε _ _)
+              ( Nεax)))
+
+  approximation-im-isometric-equiv-approximation-Metric-Space :
+    approximation-Metric-Space (l1 ⊔ l3 ⊔ l5) Y ε
+  approximation-im-isometric-equiv-approximation-Metric-Space =
+    ( im-subtype
+        ( map-isometric-equiv-Metric-Space X Y f)
+        ( subset-approximation-Metric-Space X ε A) ,
+      is-approximation-im-isometric-equiv-approximation-Metric-Space)
 ```
 
 ## References

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

@@ -30,17 +30,17 @@ if it is [totally bounded](metric-spaces.totally-bounded-metric-spaces.md) and
 
 ```agda
 module _
-  {l1 l2 : Level} (X : Metric-Space l1 l2)
+  {l1 l2 : Level} (l3 : Level) (X : Metric-Space l1 l2)
   where
 
-  is-compact-prop-Metric-Space : Prop (lsuc l1 ⊔ lsuc l2)
+  is-compact-prop-Metric-Space : Prop (l1 ⊔ l2 ⊔ lsuc l3)
   is-compact-prop-Metric-Space =
-    is-totally-bounded-prop-Metric-Space X ∧ is-complete-prop-Metric-Space X
+    is-totally-bounded-prop-Metric-Space l3 X ∧ is-complete-prop-Metric-Space X
 
-  is-compact-Metric-Space : UU (lsuc l1 ⊔ lsuc l2)
+  is-compact-Metric-Space : UU (l1 ⊔ l2 ⊔ lsuc l3)
   is-compact-Metric-Space = type-Prop is-compact-prop-Metric-Space
 
-Compact-Metric-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-Compact-Metric-Space l1 l2 =
-  type-subtype (is-compact-prop-Metric-Space {l1} {l2})
+Compact-Metric-Space : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
+Compact-Metric-Space l1 l2 l3 =
+  type-subtype (is-compact-prop-Metric-Space {l1} {l2} l3)
 ```

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

@@ -18,6 +18,8 @@ open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
 open import foundation.subtypes
 open import foundation.torsorial-type-families
 open import foundation.transport-along-identifications
@@ -82,6 +84,41 @@ module _
     isometric-equiv-Pseudometric-Space
       ( pseudometric-Metric-Space A)
       ( pseudometric-Metric-Space B)
+
+  equiv-isometric-equiv-Metric-Space :
+    isometric-equiv-Metric-Space → type-Metric-Space A ≃ type-Metric-Space B
+  equiv-isometric-equiv-Metric-Space = pr1
+
+  map-isometric-equiv-Metric-Space :
+    isometric-equiv-Metric-Space → type-Metric-Space A → type-Metric-Space B
+  map-isometric-equiv-Metric-Space e =
+    map-equiv (equiv-isometric-equiv-Metric-Space e)
+
+  map-inv-isometric-equiv-Metric-Space :
+    isometric-equiv-Metric-Space → type-Metric-Space B → type-Metric-Space A
+  map-inv-isometric-equiv-Metric-Space e =
+    map-inv-equiv (equiv-isometric-equiv-Metric-Space e)
+
+  is-section-map-inv-isometric-equiv-Metric-Space :
+    (e : isometric-equiv-Metric-Space) →
+    is-section
+      ( map-isometric-equiv-Metric-Space e)
+      ( map-inv-isometric-equiv-Metric-Space e)
+  is-section-map-inv-isometric-equiv-Metric-Space e =
+    is-section-map-inv-equiv (equiv-isometric-equiv-Metric-Space e)
+
+  is-retraction-map-inv-isometric-equiv-Metric-Space :
+    (e : isometric-equiv-Metric-Space) →
+    is-retraction
+      ( map-isometric-equiv-Metric-Space e)
+      ( map-inv-isometric-equiv-Metric-Space e)
+  is-retraction-map-inv-isometric-equiv-Metric-Space e =
+    is-retraction-map-inv-equiv (equiv-isometric-equiv-Metric-Space e)
+
+  is-isometry-map-isometric-equiv-Metric-Space :
+    (e : isometric-equiv-Metric-Space) →
+    is-isometry-Metric-Space A B (map-isometric-equiv-Metric-Space e)
+  is-isometry-map-isometric-equiv-Metric-Space = pr2
 ```
 
 ### Isometric equivalences between metric spaces