Mathlib Map

Theorems · Theorem · order theory

StrictMono.imp

∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a b : α},
  StrictMono f → a < b → f a < f b
Defined in
Mathlib.Order.Monotone.Defs
Cited by
4 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.

StrictMono.strictMonoOn · cited by 24StrictMono.strictMonoOnStrictMono.wellFoundedLT · cited by 3StrictMono.wellFoundedLTStrictMono.wellFoundedGT · cited by 2StrictMono.wellFoundedGTStrictMono.prodMap · cited by 0StrictMono.prodMapPreorder · cited by 7952PreorderStrictMono · cited by 706StrictMonoStrictMono.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
  • StrictMonostatement and proof · cited by 706

Cited by4

Results whose statement or proof uses this declaration.