Mathlib Map

Theorems · Theorem · order theory

StrictMonoOn.comp

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, StrictMonoOn g t → StrictMonoOn f s → Set.MapsTo f s t → StrictMonoOn (g ∘ f) s
Defined in
Mathlib.Order.Monotone.Defs
Cited by
2 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_arcosh · cited by 2Real.strictMonoOn_arcoshReal.strictMonoOn_artanh · cited by 2Real.strictMonoOn_artanhSet · cited by 53352SetPreorder · cited by 7952PreorderSet.MapsTo · cited by 732Set.MapsToStrictMonoOn · cited by 194StrictMonoOnStrictMonoOn.compCITED 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
  • Set.MapsTostatement and proof · cited by 732
  • StrictMonoOnstatement and proof · cited by 194

Cited by2

Results whose statement or proof uses this declaration.