Decreasing sequences in the real numbers

Content created by Louis Wasserman.

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

module real-numbers.decreasing-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.decreasing-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 decreasing if it is decreasing in the poset of real numbers.

Definition

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

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

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

Properties

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

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

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

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

Recent changes