Accumulation points of subsets of the real numbers

Content created by Louis Wasserman.

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

module real-numbers.accumulation-points-subsets-real-numbers where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.function-types
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.apartness-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.limits-sequences-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)

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

  is-sequential-accumulation-point-is-accumulation-point-subset-ℝ :
    (x : ℝ l2) → is-accumulation-point-subset-ℝ x →
    is-sequential-accumulation-point-subset-ℝ x
  is-sequential-accumulation-point-is-accumulation-point-subset-ℝ =
    is-sequential-accumulation-point-is-accumulation-point-subset-Located-Metric-Space
      ( located-metric-space-ℝ l2)
      ( S)

  is-sequence-accumulating-to-point-prop-subset-ℝ :
    ℝ l2 → subtype l2 (sequence (type-subtype S))
  is-sequence-accumulating-to-point-prop-subset-ℝ =
    is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space
      ( located-metric-space-ℝ l2)
      ( S)

  is-sequence-accumulating-to-point-subset-ℝ :
    ℝ l2 → sequence (type-subtype S) → UU l2
  is-sequence-accumulating-to-point-subset-ℝ x =
    is-in-subtype (is-sequence-accumulating-to-point-prop-subset-ℝ x)

  sequence-accumulating-to-point-subset-ℝ : ℝ l2 → UU (l1 ⊔ lsuc l2)
  sequence-accumulating-to-point-subset-ℝ x =
    type-subtype (is-sequence-accumulating-to-point-prop-subset-ℝ x)

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

Properties

Properties of a sequence accumulating to a point

module _
  {l1 l2 : Level}
  (S : subset-ℝ l1 l2)
  (x : ℝ l2)
  (y : sequence-accumulating-to-point-subset-ℝ S x)
  where

  map-sequence-accumulating-to-point-subset-ℝ : sequence (type-subtype S)
  map-sequence-accumulating-to-point-subset-ℝ = pr1 y

  real-sequence-accumulating-to-point-subset-ℝ : sequence (ℝ l2)
  real-sequence-accumulating-to-point-subset-ℝ = pr1 ∘ pr1 y

  abstract
    apart-sequence-accumulating-to-point-subset-ℝ :
      (n : ℕ) → apart-ℝ (real-sequence-accumulating-to-point-subset-ℝ n) x
    apart-sequence-accumulating-to-point-subset-ℝ n =
      apart-apart-located-metric-space-ℝ _ _ (pr1 (pr2 y) n)

    is-limit-sequence-accumulating-to-point-subset-ℝ :
      is-limit-sequence-ℝ real-sequence-accumulating-to-point-subset-ℝ x
    is-limit-sequence-accumulating-to-point-subset-ℝ =
      pr2 (pr2 y)

Recent changes