Proper closed intervals in the real numbers
Content created by Louis Wasserman.
Created on 2025-11-15.
Last modified on 2025-11-16.
module real-numbers.proper-closed-intervals-real-numbers where
Imports
open import elementary-number-theory.rational-numbers open import elementary-number-theory.unit-fractions-rational-numbers open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.existential-quantification open import foundation.identity-types open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cauchy-approximations-metric-spaces open import metric-spaces.closed-subsets-metric-spaces open import metric-spaces.complete-metric-spaces open import metric-spaces.limits-of-cauchy-approximations-metric-spaces open import metric-spaces.metric-space-of-rational-numbers open import metric-spaces.metric-spaces open import metric-spaces.short-functions-metric-spaces open import metric-spaces.subspaces-metric-spaces open import order-theory.large-posets open import real-numbers.accumulation-points-subsets-real-numbers open import real-numbers.addition-positive-real-numbers open import real-numbers.addition-real-numbers open import real-numbers.apartness-real-numbers open import real-numbers.binary-maximum-real-numbers open import real-numbers.binary-minimum-real-numbers open import real-numbers.closed-intervals-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.isometry-addition-real-numbers open import real-numbers.isometry-difference-real-numbers open import real-numbers.metric-space-of-real-numbers open import real-numbers.positive-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.similarity-real-numbers open import real-numbers.strict-inequality-real-numbers open import real-numbers.subsets-real-numbers
Idea
A proper closed interval¶ in the real numbers is a closed interval in which the lower bound is strictly less than the upper bound.
Definition
proper-closed-interval-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) proper-closed-interval-ℝ l1 l2 = Σ (ℝ l1) (λ x → Σ (ℝ l2) (λ y → le-ℝ x y)) closed-interval-proper-closed-interval-ℝ : {l1 l2 : Level} → proper-closed-interval-ℝ l1 l2 → closed-interval-ℝ l1 l2 closed-interval-proper-closed-interval-ℝ (a , b , a<b) = ((a , b) , leq-le-ℝ a<b) lower-bound-proper-closed-interval-ℝ : {l1 l2 : Level} → proper-closed-interval-ℝ l1 l2 → ℝ l1 lower-bound-proper-closed-interval-ℝ (a , b , a<b) = a upper-bound-proper-closed-interval-ℝ : {l1 l2 : Level} → proper-closed-interval-ℝ l1 l2 → ℝ l2 upper-bound-proper-closed-interval-ℝ (a , b , a<b) = b subtype-proper-closed-interval-ℝ : {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 → subset-ℝ (l1 ⊔ l2 ⊔ l) l subtype-proper-closed-interval-ℝ l (a , b , _) x = leq-prop-ℝ a x ∧ leq-prop-ℝ x b is-in-proper-closed-interval-ℝ : {l1 l2 l3 : Level} → proper-closed-interval-ℝ l1 l2 → ℝ l3 → UU (l1 ⊔ l2 ⊔ l3) is-in-proper-closed-interval-ℝ (a , b , _) x = leq-ℝ a x × leq-ℝ x b type-proper-closed-interval-ℝ : {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 → UU (l1 ⊔ l2 ⊔ lsuc l) type-proper-closed-interval-ℝ l [a,b] = type-subtype (subtype-proper-closed-interval-ℝ l [a,b])
Properties
The metric space associated with a proper closed interval
metric-space-proper-closed-interval-ℝ : {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 → Metric-Space (l1 ⊔ l2 ⊔ lsuc l) l metric-space-proper-closed-interval-ℝ l [a,b] = metric-space-closed-interval-ℝ ( l) ( closed-interval-proper-closed-interval-ℝ [a,b])
The metric space associated with a proper closed interval is closed
abstract is-closed-subset-proper-closed-interval-ℝ : {l1 l2 l3 : Level} ([a,b] : proper-closed-interval-ℝ l1 l2) → is-closed-subset-Metric-Space ( metric-space-ℝ l3) ( subtype-proper-closed-interval-ℝ l3 [a,b]) is-closed-subset-proper-closed-interval-ℝ [a,b] = is-closed-subset-closed-interval-ℝ ( closed-interval-proper-closed-interval-ℝ [a,b]) closed-subset-proper-closed-interval-ℝ : {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 → closed-subset-Metric-Space (l1 ⊔ l2 ⊔ l) (metric-space-ℝ l) closed-subset-proper-closed-interval-ℝ l [a,b] = closed-subset-closed-interval-ℝ ( l) ( closed-interval-proper-closed-interval-ℝ [a,b])
The complete metric space associated with a proper closed interval
complete-metric-space-proper-closed-interval-ℝ : {l1 l2 : Level} (l : Level) → proper-closed-interval-ℝ l1 l2 → Complete-Metric-Space (l1 ⊔ l2 ⊔ lsuc l) l complete-metric-space-proper-closed-interval-ℝ l [a,b] = complete-metric-space-closed-interval-ℝ ( l) ( closed-interval-proper-closed-interval-ℝ [a,b])
The clamp function
clamp-proper-closed-interval-ℝ : {l1 l2 l3 : Level} ([a,b] : proper-closed-interval-ℝ l1 l2) → ℝ l3 → type-proper-closed-interval-ℝ (l1 ⊔ l2 ⊔ l3) [a,b] clamp-proper-closed-interval-ℝ [a,b] = clamp-closed-interval-ℝ (closed-interval-proper-closed-interval-ℝ [a,b])
The clamp function is a short function
abstract is-short-clamp-proper-closed-interval-ℝ : {l1 l2 l3 : Level} ([a,b] : proper-closed-interval-ℝ l1 l2) → is-short-function-Metric-Space ( metric-space-ℝ l3) ( metric-space-proper-closed-interval-ℝ (l1 ⊔ l2 ⊔ l3) [a,b]) ( clamp-proper-closed-interval-ℝ [a,b]) is-short-clamp-proper-closed-interval-ℝ [a,b] = is-short-clamp-closed-interval-ℝ ( closed-interval-proper-closed-interval-ℝ [a,b]) short-clamp-proper-closed-interval-ℝ : {l1 l2 l3 : Level} ([a,b] : proper-closed-interval-ℝ l1 l2) → short-function-Metric-Space ( metric-space-ℝ l3) ( metric-space-proper-closed-interval-ℝ (l1 ⊔ l2 ⊔ l3) [a,b]) short-clamp-proper-closed-interval-ℝ [a,b] = short-clamp-closed-interval-ℝ (closed-interval-proper-closed-interval-ℝ [a,b])
Every real number in a proper closed interval is an accumulation point in that proper closed interval
Note that this cannot be made more universe-polymorphic.
abstract is-accumulation-point-le-upper-bound-proper-closed-interval-ℝ : {l : Level} ([a,b] : proper-closed-interval-ℝ l l) → (x : ℝ l) → is-in-proper-closed-interval-ℝ [a,b] x → le-ℝ x (upper-bound-proper-closed-interval-ℝ [a,b]) → is-accumulation-point-subset-ℝ ( subtype-proper-closed-interval-ℝ l [a,b]) ( x) is-accumulation-point-le-upper-bound-proper-closed-interval-ℝ {l} [a,b]@(a , b , a<b) x (a≤x , x≤b) x<b = let open inequality-reasoning-Large-Poset ℝ-Large-Poset motive = is-accumulation-point-prop-subset-ℝ ( subtype-proper-closed-interval-ℝ _ [a,b]) ( x) short-clamp-add = comp-short-function-Metric-Space ( metric-space-ℚ) ( metric-space-ℝ lzero) ( metric-space-proper-closed-interval-ℝ l [a,b]) ( comp-short-function-Metric-Space ( metric-space-ℝ lzero) ( metric-space-ℝ l) ( metric-space-proper-closed-interval-ℝ l [a,b]) ( short-clamp-proper-closed-interval-ℝ [a,b]) ( short-left-add-ℝ x)) ( short-isometry-Metric-Space ( metric-space-ℚ) ( metric-space-ℝ lzero) ( isometry-metric-space-real-ℚ)) short-inclusion = short-inclusion-subspace-Metric-Space ( metric-space-ℝ l) ( subtype-proper-closed-interval-ℝ l [a,b]) approx-clamp-add = map-short-function-cauchy-approximation-Metric-Space ( metric-space-ℚ) ( metric-space-proper-closed-interval-ℝ l [a,b]) ( short-clamp-add) ( cauchy-approximation-rational-ℚ⁺) in intro-exists ( approx-clamp-add) ( ( λ ε → apart-located-metric-space-apart-ℝ _ _ ( apart-le-ℝ' ( concatenate-le-leq-ℝ ( x) ( min-ℝ b (x +ℝ real-ℚ⁺ ε)) ( max-ℝ a (min-ℝ b (x +ℝ real-ℚ⁺ ε))) ( le-min-le-le-ℝ ( x<b) ( le-left-add-real-ℝ⁺ x (positive-real-ℚ⁺ ε))) ( leq-right-max-ℝ _ _)))) , tr ( is-limit-cauchy-approximation-Metric-Space ( metric-space-ℝ l) ( map-short-function-cauchy-approximation-Metric-Space ( metric-space-proper-closed-interval-ℝ l [a,b]) ( metric-space-ℝ l) ( short-inclusion) ( approx-clamp-add))) ( equational-reasoning max-ℝ a (min-ℝ b (x +ℝ zero-ℝ)) ＝ max-ℝ a (min-ℝ b x) by ap-max-ℝ refl (ap-min-ℝ refl (right-unit-law-add-ℝ x)) ＝ max-ℝ a x by ap-max-ℝ refl (eq-sim-ℝ (right-leq-left-min-ℝ x≤b)) ＝ x by eq-sim-ℝ (left-leq-right-max-ℝ a≤x)) ( preserves-limit-cauchy-approximation-map-short-function-Metric-Space ( metric-space-ℚ) ( metric-space-ℝ l) ( comp-short-function-Metric-Space ( metric-space-ℚ) ( metric-space-proper-closed-interval-ℝ l [a,b]) ( metric-space-ℝ l) ( short-inclusion) ( short-clamp-add)) ( cauchy-approximation-rational-ℚ⁺) ( zero-ℚ) ( is-zero-limit-rational-ℚ⁺))) is-accumulation-point-le-lower-bound-proper-closed-interval-ℝ : {l : Level} ([a,b] : proper-closed-interval-ℝ l l) → (x : ℝ l) → is-in-proper-closed-interval-ℝ [a,b] x → le-ℝ (lower-bound-proper-closed-interval-ℝ [a,b]) x → is-accumulation-point-subset-ℝ ( subtype-proper-closed-interval-ℝ l [a,b]) ( x) is-accumulation-point-le-lower-bound-proper-closed-interval-ℝ {l} [a,b]@(a , b , a<b) x (a≤x , x≤b) a<x = let open inequality-reasoning-Large-Poset ℝ-Large-Poset motive = is-accumulation-point-prop-subset-ℝ ( subtype-proper-closed-interval-ℝ _ [a,b]) ( x) short-clamp-diff = comp-short-function-Metric-Space ( metric-space-ℚ) ( metric-space-ℝ lzero) ( metric-space-proper-closed-interval-ℝ l [a,b]) ( comp-short-function-Metric-Space ( metric-space-ℝ lzero) ( metric-space-ℝ l) ( metric-space-proper-closed-interval-ℝ l [a,b]) ( short-clamp-proper-closed-interval-ℝ [a,b]) ( short-diff-ℝ x)) ( short-isometry-Metric-Space ( metric-space-ℚ) ( metric-space-ℝ lzero) ( isometry-metric-space-real-ℚ)) short-inclusion = short-inclusion-subspace-Metric-Space ( metric-space-ℝ l) ( subtype-proper-closed-interval-ℝ l [a,b]) approx-clamp-diff = map-short-function-cauchy-approximation-Metric-Space ( metric-space-ℚ) ( metric-space-proper-closed-interval-ℝ l [a,b]) ( short-clamp-diff) ( cauchy-approximation-rational-ℚ⁺) in intro-exists ( approx-clamp-diff) ( ( λ ε → apart-located-metric-space-apart-ℝ _ _ ( apart-le-ℝ ( le-max-le-le-ℝ ( a<x) ( concatenate-leq-le-ℝ ( min-ℝ b (x -ℝ real-ℚ⁺ ε)) ( x -ℝ real-ℚ⁺ ε) ( x) ( leq-right-min-ℝ _ _) ( le-diff-real-ℝ⁺ x (positive-real-ℚ⁺ ε)))))) , tr ( is-limit-cauchy-approximation-Metric-Space ( metric-space-ℝ l) ( map-short-function-cauchy-approximation-Metric-Space ( metric-space-proper-closed-interval-ℝ l [a,b]) ( metric-space-ℝ l) ( short-inclusion) ( approx-clamp-diff))) ( equational-reasoning max-ℝ a (min-ℝ b (x -ℝ zero-ℝ)) ＝ max-ℝ a (min-ℝ b x) by ap-max-ℝ refl (ap-min-ℝ refl (right-unit-law-diff-ℝ x)) ＝ max-ℝ a x by ap-max-ℝ refl (eq-sim-ℝ (right-leq-left-min-ℝ x≤b)) ＝ x by eq-sim-ℝ (left-leq-right-max-ℝ a≤x)) ( preserves-limit-cauchy-approximation-map-short-function-Metric-Space ( metric-space-ℚ) ( metric-space-ℝ l) ( comp-short-function-Metric-Space ( metric-space-ℚ) ( metric-space-proper-closed-interval-ℝ l [a,b]) ( metric-space-ℝ l) ( short-inclusion) ( short-clamp-diff)) ( cauchy-approximation-rational-ℚ⁺) ( zero-ℚ) ( is-zero-limit-rational-ℚ⁺))) is-accumulation-point-is-in-proper-closed-interval-ℝ : {l : Level} ([a,b] : proper-closed-interval-ℝ l l) → (x : ℝ l) → is-in-proper-closed-interval-ℝ [a,b] x → is-accumulation-point-subset-ℝ ( subtype-proper-closed-interval-ℝ l [a,b]) ( x) is-accumulation-point-is-in-proper-closed-interval-ℝ {l} [a,b]@(a , b , a<b) x a≤x≤b = elim-disjunction ( is-accumulation-point-prop-subset-ℝ ( subtype-proper-closed-interval-ℝ _ [a,b]) ( x)) ( is-accumulation-point-le-lower-bound-proper-closed-interval-ℝ ( [a,b]) ( x) ( a≤x≤b)) ( is-accumulation-point-le-upper-bound-proper-closed-interval-ℝ ( [a,b]) ( x) ( a≤x≤b)) ( cotransitive-le-ℝ a b x a<b)
Recent changes
- 2025-11-16. Louis Wasserman. Multiplicative inverses of nonzero complex numbers (#1684).
- 2025-11-15. Louis Wasserman. Every point in a proper closed interval in the real numbers is an accumulation point (#1679).