Decreasing sequences in posets

Content created by Louis Wasserman.

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

module order-theory.decreasing-sequences-posets where
Imports 
open import elementary-number-theory.natural-numbers

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

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

Idea

A sequence in a poset is decreasing if it is increasing in the opposite poset.

Definition

module _
  {l1 l2 : Level}
  (P : Poset l1 l2)
  where

  is-decreasing-prop-sequence-Poset : sequence-type-Poset P → Prop l2
  is-decreasing-prop-sequence-Poset =
    is-increasing-prop-sequence-Poset (opposite-Poset P)

  is-decreasing-sequence-Poset : sequence-type-Poset P → UU l2
  is-decreasing-sequence-Poset u =
    type-Prop (is-decreasing-prop-sequence-Poset u)

Properties

A sequence u in a poset is decreasing if and only if uₙ₊₁ ≤ uₙ for all n : ℕ

module _
  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-type-Poset P)
  where

  abstract
    is-decreasing-leq-succ-sequence-Poset :
      ((n : ℕ) → leq-Poset P (u (succ-ℕ n)) (u n)) →
      is-decreasing-sequence-Poset P u
    is-decreasing-leq-succ-sequence-Poset =
      is-increasing-leq-succ-sequence-Poset (opposite-Poset P) u

    leq-succ-is-decreasing-sequence-Poset :
      is-decreasing-sequence-Poset P u →
      ((n : ℕ) → leq-Poset P (u (succ-ℕ n)) (u n))
    leq-succ-is-decreasing-sequence-Poset =
      leq-succ-is-increasing-sequence-Poset (opposite-Poset P) u

Recent changes