Closed subsets of located metric spaces

Content created by Louis Wasserman.

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

module metric-spaces.closed-subsets-located-metric-spaces where
Imports 
open import foundation.propositions
open import foundation.universe-levels

open import metric-spaces.closed-subsets-metric-spaces
open import metric-spaces.located-metric-spaces
open import metric-spaces.metric-spaces

Idea

A subset S of a located metric space X is closed if it is a closed subset of the underlying metric space

Definition

module _
  {l1 l2 l3 : Level}
  (X : Located-Metric-Space l1 l2) (S : subset-Located-Metric-Space l3 X)
  where

  is-closed-prop-subset-Located-Metric-Space : Prop (l1 ⊔ l2 ⊔ l3)
  is-closed-prop-subset-Located-Metric-Space =
    is-closed-prop-subset-Metric-Space
      ( metric-space-Located-Metric-Space X)
      ( S)

  is-closed-subset-Located-Metric-Space : UU (l1 ⊔ l2 ⊔ l3)
  is-closed-subset-Located-Metric-Space =
    type-Prop is-closed-prop-subset-Located-Metric-Space

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

Recent changes