Mathlib Map

Theorems · Theorem · order theory

StrictMono.comp_strictMonoOn

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α}, StrictMono g → StrictMonoOn f s → StrictMonoOn (g ∘ f) s
Defined in
Mathlib.Order.Monotone.Defs
Cited by
4 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
PreorderPreorderPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Real.strictMonoOn_arcsin · cited by 4Real.strictMonoOn_arcsinStrictMono.strictMonoOn_IccExtend · cited by 1StrictMono.strictMonoOn_I…StrictMono.strictMonoOn_IciExtend · cited by 0StrictMono.strictMonoOn_I…StrictMono.strictMonoOn_IicExtend · cited by 0StrictMono.strictMonoOn_I…Set · cited by 53352SetPreorder · cited by 7952PreorderStrictMono · cited by 706StrictMonoStrictMonoOn · cited by 194StrictMonoOnStrictMono.comp_strictMonoOnCITED BYCITES

Cites4

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

  • Setstatement and proof · cited by 53,352
  • Preorderstatement and proof · cited by 7,952
  • StrictMonostatement and proof · cited by 706
  • StrictMonoOnstatement and proof · cited by 194

Cited by4

Results whose statement or proof uses this declaration.