Closed interval preserving endomaps on the rational numbers

Content created by Louis Wasserman.

Created on 2025-10-07.
Last modified on 2025-10-07.

module elementary-number-theory.closed-interval-preserving-maps-rational-numbers where
Imports 
open import elementary-number-theory.closed-intervals-rational-numbers
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.rational-numbers

open import foundation.propositions
open import foundation.universe-levels

open import order-theory.closed-interval-preserving-maps-posets

Idea

A map from the rational numbers to themselves f : ℚ → ℚ is closed interval preserving if the image of a closed interval is always a closed interval in Y. Equivalently, it is a closed interval preserving map on the total order of rational numbers.

Definition

is-closed-interval-map-ℚ :
  (ℚ → ℚ) → ([a,b] [c,d] : closed-interval-ℚ) → UU lzero
is-closed-interval-map-ℚ = is-closed-interval-map-Poset ℚ-Poset ℚ-Poset

is-closed-interval-map-prop-ℚ :
  (ℚ → ℚ) → closed-interval-ℚ → closed-interval-ℚ →
  Prop lzero
is-closed-interval-map-prop-ℚ =
  is-closed-interval-map-prop-Poset ℚ-Poset ℚ-Poset

Recent changes