Totally bounded metric spaces
Content created by Louis Wasserman and Fredrik Bakke.
Created on 2025-08-30.
Last modified on 2026-01-30.
module metric-spaces.totally-bounded-metric-spaces where
Imports
open import elementary-number-theory.positive-rational-numbers open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.function-types open import foundation.functoriality-propositional-truncation open import foundation.images open import foundation.inhabited-types open import foundation.propositional-truncations open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cartesian-products-metric-spaces open import metric-spaces.equality-of-metric-spaces open import metric-spaces.images-isometries-metric-spaces open import metric-spaces.images-metric-spaces open import metric-spaces.images-short-maps-metric-spaces open import metric-spaces.images-uniformly-continuous-maps-metric-spaces open import metric-spaces.isometries-metric-spaces open import metric-spaces.maps-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.modulated-uniformly-continuous-maps-metric-spaces open import metric-spaces.nets-metric-spaces open import metric-spaces.short-maps-metric-spaces open import metric-spaces.uniform-homeomorphisms-metric-spaces open import metric-spaces.uniformly-continuous-maps-metric-spaces open import univalent-combinatorics.finitely-enumerable-subtypes
Idea
A metric space is
totally bounded¶
if for every ε : ℚ⁺, it has an ε-net.
Definitions
The property of a space being totally bounded
module _ {l1 l2 : Level} (l3 : Level) (X : Metric-Space l1 l2) where modulus-of-total-boundedness-Metric-Space : UU (l1 ⊔ l2 ⊔ lsuc l3) modulus-of-total-boundedness-Metric-Space = (ε : ℚ⁺) → net-Metric-Space l3 X ε is-totally-bounded-prop-Metric-Space : Prop (l1 ⊔ l2 ⊔ lsuc l3) is-totally-bounded-prop-Metric-Space = trunc-Prop modulus-of-total-boundedness-Metric-Space is-totally-bounded-Metric-Space : UU (l1 ⊔ l2 ⊔ lsuc l3) is-totally-bounded-Metric-Space = type-Prop is-totally-bounded-prop-Metric-Space
Totally bounded metric spaces
Totally-Bounded-Metric-Space : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) Totally-Bounded-Metric-Space l1 l2 l3 = Σ (Metric-Space l1 l2) (is-totally-bounded-Metric-Space l3) module _ {l1 l2 l3 : Level} (M : Totally-Bounded-Metric-Space l1 l2 l3) where metric-space-Totally-Bounded-Metric-Space : Metric-Space l1 l2 metric-space-Totally-Bounded-Metric-Space = pr1 M is-totally-bounded-metric-space-Totally-Bounded-Metric-Space : is-totally-bounded-Metric-Space l3 metric-space-Totally-Bounded-Metric-Space is-totally-bounded-metric-space-Totally-Bounded-Metric-Space = pr2 M
Properties
The image of a totally bounded metric space under a uniformly continuous map is totally bounded
module _ {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (μX : modulus-of-total-boundedness-Metric-Space l5 X) (f : map-Metric-Space X Y) {μf : ℚ⁺ → ℚ⁺} (is-muc-μf : is-modulus-of-uniform-continuity-map-Metric-Space X Y f μf) where modulus-of-total-boundedness-im-modulated-uniformly-continuous-map-Metric-Space : modulus-of-total-boundedness-Metric-Space ( l1 ⊔ l3 ⊔ l5) ( im-Metric-Space X Y f) modulus-of-total-boundedness-im-modulated-uniformly-continuous-map-Metric-Space ε = net-im-uniformly-continuous-map-net-Metric-Space X Y f ( is-muc-μf) ( ε) ( μX (μf ε)) module _ {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (tbX : is-totally-bounded-Metric-Space l5 X) (f : uniformly-continuous-map-Metric-Space X Y) where abstract is-totally-bounded-im-uniformly-continuous-map-is-totally-bounded-Metric-Space : is-totally-bounded-Metric-Space ( l1 ⊔ l3 ⊔ l5) ( im-uniformly-continuous-map-Metric-Space X Y f) is-totally-bounded-im-uniformly-continuous-map-is-totally-bounded-Metric-Space = let open do-syntax-trunc-Prop ( is-totally-bounded-prop-Metric-Space ( l1 ⊔ l3 ⊔ l5) ( im-uniformly-continuous-map-Metric-Space X Y f)) in do (_ , μf) ← is-uniformly-continuous-map-uniformly-continuous-map-Metric-Space ( X) ( Y) ( f) μX ← tbX unit-trunc-Prop ( modulus-of-total-boundedness-im-modulated-uniformly-continuous-map-Metric-Space ( X) ( Y) ( μX) ( map-uniformly-continuous-map-Metric-Space X Y f) ( μf))
The image of a totally bounded metric space under a short map is totally bounded
module _ {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (tbX : is-totally-bounded-Metric-Space l5 X) (f : short-map-Metric-Space X Y) where abstract is-totally-bounded-im-short-map-is-totally-bounded-Metric-Space : is-totally-bounded-Metric-Space ( l1 ⊔ l3 ⊔ l5) ( im-short-map-Metric-Space X Y f) is-totally-bounded-im-short-map-is-totally-bounded-Metric-Space = is-totally-bounded-im-uniformly-continuous-map-is-totally-bounded-Metric-Space ( X) ( Y) ( tbX) ( uniformly-continuous-map-short-map-Metric-Space X Y f)
The image of a totally bounded metric space under an isometry is totally bounded
module _ {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (tbX : is-totally-bounded-Metric-Space l5 X) (f : isometry-Metric-Space X Y) where abstract is-totally-bounded-im-isometry-is-totally-bounded-Metric-Space : is-totally-bounded-Metric-Space ( l1 ⊔ l3 ⊔ l5) ( im-isometry-Metric-Space X Y f) is-totally-bounded-im-isometry-is-totally-bounded-Metric-Space = is-totally-bounded-im-short-map-is-totally-bounded-Metric-Space ( X) ( Y) ( tbX) ( short-map-isometry-Metric-Space X Y f)
Total boundedness is preserved by isometric equivalences
module _ {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (tbX : is-totally-bounded-Metric-Space l5 X) (f : isometric-equiv-Metric-Space X Y) where abstract preserves-is-totally-bounded-isometric-equiv-Metric-Space : is-totally-bounded-Metric-Space (l1 ⊔ l3 ⊔ l5) Y preserves-is-totally-bounded-isometric-equiv-Metric-Space = map-is-inhabited ( λ μX ε → net-im-isometric-equiv-net-Metric-Space X Y f ε (μX ε)) ( tbX)
Totally bounded metric spaces are closed under cartesian products
abstract is-totally-bounded-product-Totally-Bounded-Metric-Space : {l1 l2 l3 l4 l5 l6 : Level} → (X : Totally-Bounded-Metric-Space l1 l2 l3) → (Y : Totally-Bounded-Metric-Space l4 l5 l6) → is-totally-bounded-Metric-Space ( l3 ⊔ l6) ( product-Metric-Space ( metric-space-Totally-Bounded-Metric-Space X) ( metric-space-Totally-Bounded-Metric-Space Y)) is-totally-bounded-product-Totally-Bounded-Metric-Space (X , tbX) (Y , tbY) = let open do-syntax-trunc-Prop ( is-totally-bounded-prop-Metric-Space _ ( product-Metric-Space X Y)) in do mX ← tbX mY ← tbY unit-trunc-Prop ( λ ε → product-net-Metric-Space X Y ε (mX ε) (mY ε)) product-Totally-Bounded-Metric-Space : {l1 l2 l3 l4 l5 l6 : Level} → (X : Totally-Bounded-Metric-Space l1 l2 l3) → (Y : Totally-Bounded-Metric-Space l4 l5 l6) → Totally-Bounded-Metric-Space (l1 ⊔ l4) (l2 ⊔ l5) (l3 ⊔ l6) product-Totally-Bounded-Metric-Space (X , tbX) (Y , tbY) = ( product-Metric-Space X Y , is-totally-bounded-product-Totally-Bounded-Metric-Space (X , tbX) (Y , tbY))
The property of being totally bounded is preserved by uniform homeomorphisms
module _ {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (f : uniform-homeo-Metric-Space X Y) where abstract preserves-is-totally-bounded-uniform-homeo-Metric-Space : is-totally-bounded-Metric-Space l5 X → is-totally-bounded-Metric-Space (l1 ⊔ l3 ⊔ l5) Y preserves-is-totally-bounded-uniform-homeo-Metric-Space = map-binary-trunc-Prop ( λ (μf , is-mod-μf) μtbX ε → let (SX , is-net-SX) = μtbX (μf ε) SY : finitely-enumerable-subtype (l1 ⊔ l3 ⊔ l5) (type-Metric-Space Y) SY = im-finitely-enumerable-subtype ( map-uniform-homeo-Metric-Space X Y f) ( SX) in ( SY , λ y → let open do-syntax-trunc-Prop ( ∃ ( type-finitely-enumerable-subtype SY) ( λ (y' , _) → neighborhood-prop-Metric-Space Y ε y' y)) in do let x = map-inv-uniform-homeo-Metric-Space X Y f y ((x' , x'∈SX) , Nμfεxx') ← is-net-SX x intro-exists ( map-unit-im ( map-uniform-homeo-Metric-Space X Y f ∘ pr1) ( x' , x'∈SX)) ( tr ( neighborhood-Metric-Space Y ε _) ( is-section-map-inv-uniform-homeo-Metric-Space ( X) ( Y) ( f) ( y)) ( is-mod-μf x' ε x Nμfεxx')))) ( is-uniformly-continuous-map-uniform-homeo-Metric-Space X Y f)
External links
- Totally bounded space at Wikidata
Recent changes
- 2026-01-30. Louis Wasserman. Refactor differentiable functions (#1774).
- 2026-01-01. Louis Wasserman and Fredrik Bakke. Use map terminology consistently in metric spaces (#1778).
- 2025-10-19. Louis Wasserman. Adding limits and Cauchy sequences in the real numbers (#1603).
- 2025-09-11. Louis Wasserman. Inhabited totally bounded subspaces of metric spaces (#1542).
- 2025-09-04. Louis Wasserman. Suprema and infima of totally bounded subsets of the reals (#1510).