Increasing sequences in the real numbers

Content created by Louis Wasserman.

Created on 2025-12-30.
Last modified on 2025-12-30.

module real-numbers.increasing-sequences-real-numbers where
Imports 
open import elementary-number-theory.natural-numbers

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

open import lists.sequences

open import order-theory.increasing-sequences-posets
open import order-theory.posets

open import real-numbers.dedekind-real-numbers
open import real-numbers.inequality-real-numbers

Idea

A sequence of real numbers is increasing if it is increasing in the poset of real numbers.

Definition

module _
  {l : Level}
  (u : sequence (ℝ l))
  where

  is-increasing-prop-sequence-ℝ : Prop l
  is-increasing-prop-sequence-ℝ =
    is-increasing-prop-sequence-Poset (ℝ-Poset l) u

  is-increasing-sequence-ℝ : UU l
  is-increasing-sequence-ℝ = type-Prop is-increasing-prop-sequence-ℝ

Properties

aₙ is increasing if and only if for all n, aₙ ≤ aₙ₊₁

module _
  {l : Level}
  (u : sequence (ℝ l))
  where

  abstract
    is-increasing-leq-succ-sequence-ℝ :
      ((n : ℕ) → leq-ℝ (u n) (u (succ-ℕ n))) → is-increasing-sequence-ℝ u
    is-increasing-leq-succ-sequence-ℝ =
      is-increasing-leq-succ-sequence-Poset (ℝ-Poset l) u

    leq-succ-is-increasing-sequence-ℝ :
      is-increasing-sequence-ℝ u → (n : ℕ) → leq-ℝ (u n) (u (succ-ℕ n))
    leq-succ-is-increasing-sequence-ℝ =
      leq-succ-is-increasing-sequence-Poset (ℝ-Poset l) u

Recent changes