Theorems · Theorem · order theory

Monotone.seq_pos_lt_seq_of_le_of_lt

∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x y : ℕ → α},
  Monotone f →
    ∀ {n : ℕ}, 0 < n → x 0 ≤ y 0 → (∀ k < n, x (k + 1) ≤ f (x k)) → (∀ k < n, f (y k) < y (k + 1)) → x n < y n

Defined in: Mathlib.Order.Iterate
Cited by: 2 results in Mathlib
Foundations: Depth 22 from the axioms · uses propext, Quot.sound
Assumes: Preorder

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Preorderstatement and proof · cited by 7,952
Monotonestatement and proof · cited by 1,397
Monotone.dualproof · cited by 39
Monotone.seq_pos_lt_seq_of_lt_of_leproof · cited by 3

Cited by2

Results whose statement or proof uses this declaration.

Function.Commute.iterate_pos_lt_of_map_ltproof · cited by 1
geom_ltproof · cited by 0