Limits of endomaps on the real numbers

Content created by Louis Wasserman.

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

module real-numbers.limits-of-endomaps-real-numbers where
Imports 
open import foundation.propositions
open import foundation.universe-levels

open import metric-spaces.limits-of-maps-metric-spaces

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

Idea

A limit of an endomap f on the real numbers at x : ℝ is the limit of f at x in the metric space of real numbers.

Definition

is-limit-prop-endomap-ℝ :
  {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → Prop (lsuc l1 ⊔ l2)
is-limit-prop-endomap-ℝ {l1} {l2} =
  is-point-limit-prop-map-Metric-Space
    ( metric-space-ℝ l1)
    ( metric-space-ℝ l2)

is-limit-endomap-ℝ :
  {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → UU (lsuc l1 ⊔ l2)
is-limit-endomap-ℝ f x y = type-Prop (is-limit-prop-endomap-ℝ f x y)

Recent changes