Proper rational neighborhood subtypes

Content created by malarbol.

Created on 2026-10-18.
Last modified on 2026-10-18.

module metric-spaces.proper-rational-neighborhood-subtypes where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-products-propositions
open import foundation.function-types
open import foundation.identity-types
open import foundation.inhabited-subtypes
open import foundation.propositions
open import foundation.universe-levels

open import metric-spaces.rational-neighborhood-subtypes

Idea

A rational neighborhood subtype U : ℚ⁺ → subtype l A is called proper if it is inhabited for all radius ε:

  ∀ (ε : ℚ⁺) → ∃ (x : A) (U ε x)

Definitions

Proper rational neighborhood subtypes

module _
  {l1 l : Level} {A : UU l1} (U : Rational-Neighborhood-Subtype l A)
  where

  is-proper-prop-Rational-Neighborhood-Subtype : Prop (l1 ⊔ l)
  is-proper-prop-Rational-Neighborhood-Subtype =
    Π-Prop ℚ⁺ (is-inhabited-subtype-Prop ∘ U)

  is-proper-Rational-Neighborhood-Subtype : UU (l1 ⊔ l)
  is-proper-Rational-Neighborhood-Subtype =
    type-Prop is-proper-prop-Rational-Neighborhood-Subtype

  is-prop-is-proper-Rational-Neighborhood-Subtype :
    is-prop is-proper-Rational-Neighborhood-Subtype
  is-prop-is-proper-Rational-Neighborhood-Subtype =
    is-prop-type-Prop is-proper-prop-Rational-Neighborhood-Subtype

Recent changes