Accumulation points of subsets of the real numbers

Content created by Louis Wasserman.

Created on 2025-11-15.
Last modified on 2025-11-15.

module real-numbers.accumulation-points-subsets-real-numbers where
Imports 
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import lists.sequences

open import metric-spaces.accumulation-points-subsets-located-metric-spaces

open import real-numbers.dedekind-real-numbers
open import real-numbers.located-metric-space-of-real-numbers
open import real-numbers.subsets-real-numbers

Idea

An accumulation point of a subset S of the real numbers is an accumulation point of S in the located metric space of the real numbers.

Accumulation points of subsets of ℝ

module _
  {l1 l2 : Level} (S : subset-ℝ l1 l2)
  where

  is-accumulation-point-prop-subset-ℝ : subset-ℝ (l1 ⊔ lsuc l2) l2
  is-accumulation-point-prop-subset-ℝ =
    is-accumulation-point-prop-subset-Located-Metric-Space
      ( located-metric-space-ℝ l2)
      ( S)

  is-accumulation-point-subset-ℝ : ℝ l2 → UU (l1 ⊔ lsuc l2)
  is-accumulation-point-subset-ℝ x =
    type-Prop (is-accumulation-point-prop-subset-ℝ x)

  accumulation-point-subset-ℝ : UU (l1 ⊔ lsuc l2)
  accumulation-point-subset-ℝ = type-subtype is-accumulation-point-prop-subset-ℝ

Recent changes