Nets in located metric spaces

Content created by Louis Wasserman.

Created on 2025-08-30.
Last modified on 2025-08-30.

module metric-spaces.nets-located-metric-spaces where
Imports 
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.existential-quantification
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.singleton-subtypes
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import metric-spaces.approximations-metric-spaces
open import metric-spaces.located-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.nets-metric-spaces

open import univalent-combinatorics.finite-subtypes
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.finitely-enumerable-subtypes
open import univalent-combinatorics.finitely-enumerable-types
open import univalent-combinatorics.standard-finite-types

Idea

For an ε : ℚ⁺, an ε-net to a located metric space X is an ε-net in the underlying metric space.

Definition

net-Located-Metric-Space :
  {l1 l2 : Level} (l3 : Level) → Located-Metric-Space l1 l2 → ℚ⁺ →
  UU (l1 ⊔ l2 ⊔ lsuc l3)
net-Located-Metric-Space l3 X =
  net-Metric-Space l3 (metric-space-Located-Metric-Space X)

Recent changes