Theorems · Theorem · order theory
monotone_add_nat_iff_monotoneOn_nat_Ici
∀ {α : Type u} [inst : Preorder α] {f : ℕ → α} {k : ℕ}, (Monotone fun n => f (n + k)) ↔ MonotoneOn f {x | k ≤ x}- Defined in
- Mathlib.Order.Monotone.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext
- Assumes
- Preorder
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
- Set.ofPredstatement and proof · cited by 6,101
- Monotonestatement and proof · cited by 1,397
- MonotoneOnstatement and proof · cited by 311
Cited by2
Results whose statement or proof uses this declaration.
- Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Iciproof · cited by 1
- antitone_add_nat_iff_antitoneOn_nat_Iciproof · cited by 1