Monotone sequences

TheoremSuccessor criterion for monotone sequences#✓fully proved

Let \(\alpha\) be a preordered set. A sequence \(f : \mathbb{N} \to \alpha\) is monotone (that is, \(f(m) \le f(n)\) whenever \(m \le n\)) if and only if \(f(n) \le f(n+1)\) for every \(n \in \mathbb{N}\).

theorem monotone_nat_iff_le_succ : Monotone f ↔ ∀ n, f n ≤ f (n + 1)

Used by 1

Used bySuccessor criterion for monotone or antitone sequences

TheoremSuccessor criterion for antitone sequences#✓fully proved

Let \(\alpha\) be a preordered set. A sequence \(f : \mathbb{N} \to \alpha\) is antitone (that is, \(f(n) \le f(m)\) whenever \(m \le n\)) if and only if \(f(n+1) \le f(n)\) for every \(n \in \mathbb{N}\).

theorem antitone_nat_iff_succ_le : Antitone f ↔ ∀ n, f (n + 1) ≤ f n

Used by 1

Used bySuccessor criterion for monotone or antitone sequences

TheoremSuccessor criterion for monotone or antitone sequences#✓fully proved

Let \(\alpha\) be a preordered set and let \(f : \mathbb{N} \to \alpha\) be a sequence. Then \(f\) is monotone (\(f(m) \le f(n)\) whenever \(m \le n\)) or antitone (\(f(n) \le f(m)\) whenever \(m \le n\)) if and only if either \(f(n) \le f(n+1)\) for every \(n \in \mathbb{N}\), or \(f(n+1) \le f(n)\) for every \(n \in \mathbb{N}\).

theorem monotone_or_antitone_nat_iff :
    Monotone f ∨ Antitone f ↔
      (∀ n, f n ≤ f (n + 1)) ∨ ∀ n, f (n + 1) ≤ f n

Uses 2

Proof usesSuccessor criterion for antitone sequences · Successor criterion for monotone sequences

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.