Functions between proper closed intervals of real numbers

Content created by malarbol.

Created on 2026-05-09.
Last modified on 2026-05-09.

{-# OPTIONS --lossy-unification #-}

module real-numbers.maps-between-proper-closed-intervals-real-numbers where
Imports 
open import foundation.function-types
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.proper-closed-intervals-real-numbers

Idea

The type of maps between proper closed intervals of real numbers I and J is the type of functions I → J, i.e., the type of real maps on I with values in J.

Definition

Maps between proper closed intervals of real numbers

module _
  {l1 l2 l3 l4 : Level} (l l' : Level)
  (I : proper-closed-interval-ℝ l1 l2)
  (J : proper-closed-interval-ℝ l3 l4)
  where

  map-proper-closed-interval-ℝ :
    UU (lsuc l ⊔ lsuc l' ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
  map-proper-closed-interval-ℝ =
    type-proper-closed-interval-ℝ l I → type-proper-closed-interval-ℝ l' J

Properties

The identity map on a proper closed interval

module _
  {l1 l2 l3 l4 : Level} (l : Level)
  (I : proper-closed-interval-ℝ l1 l2)
  where

  id-proper-closed-interval-ℝ : map-proper-closed-interval-ℝ l l I I
  id-proper-closed-interval-ℝ = id

Composition of maps between proper closed intervals

module _
  {l1 l2 l3 l4 l5 l6 l l' l'' : Level}
  {I : proper-closed-interval-ℝ l1 l2}
  {J : proper-closed-interval-ℝ l3 l4}
  {K : proper-closed-interval-ℝ l5 l6}
  (g : map-proper-closed-interval-ℝ l' l'' J K)
  (f : map-proper-closed-interval-ℝ l l' I J)
  where

  comp-map-proper-closed-interval-ℝ : map-proper-closed-interval-ℝ l l'' I K
  comp-map-proper-closed-interval-ℝ = g ∘ f

Recent changes