Mathlib Map

Theorems · Theorem · order theory

Monotone.imp

∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a b : α},
  Monotone f → a ≤ b → f a ≤ f b
Defined in
Mathlib.Order.Monotone.Defs
Cited by
3 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
PreorderPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Monotone.monotoneOn · cited by 43Monotone.monotoneOnNat.cast_add_one_pos · cited by 18Nat.cast_add_one_posStrictMono.prodMap · cited by 0StrictMono.prodMapPreorder · cited by 7952PreorderMonotone · cited by 1397MonotoneMonotone.impCITED BYCITES

Cites2

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

Cited by3

Results whose statement or proof uses this declaration.