Saturated rational neighborhood subtypes

Content created by malarbol.

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

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

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.dependent-products-propositions
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import metric-spaces.rational-neighborhood-subtypes

Idea

A rational neighborhood subtype U : ℚ⁺ → subtype l A is called saturated if for any radius ε : ℚ⁺, U ε contains the intersection of U δ for all ε < δ: ∩ (ε < δ) Uδ ⊆ Uε, or, equivalently, for any point x : A

  (∀ (δ : ℚ⁺) → U (ε + δ) x) ⇒ U ε x

Definitions

Saturated rational neighborhood subtypes

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

  is-saturated-prop-Rational-Neighborhood-Subtype : Prop (l1 ⊔ l)
  is-saturated-prop-Rational-Neighborhood-Subtype =
    Π-Prop
      ( ℚ⁺ × A)
      ( λ (ε , x) → (Π-Prop ℚ⁺ (λ δ → U (ε +ℚ⁺ δ) x)) ⇒ (U ε x))

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

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

Recent changes