Mathlib Map

Theorems · Theorem · order theory

StrictMono.comp

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

Around this declaration

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

Ordinal.cof_map_of_isNormal · cited by 7Ordinal.cof_map_of_isNorm…Nat.nth_strictMono · cited by 6Nat.nth_strictMonoEReal.coe_strictMono · cited by 6EReal.coe_strictMonoOrder.IsNormal.comp · cited by 5IsNormal.compIsSeqCompact.subseq_of_frequently_in · cited by 5IsSeqCompact.subseq_of_fr…WithTop.strictMono_iff · cited by 4WithTop.strictMono_iffCardinal.IsInaccessible.preAleph_ord · cited by 3IsInaccessible.preAleph_o…Cardinal.IsInaccessible.preBeth_ord · cited by 3IsInaccessible.preBeth_ordCardinal.beth_strictMono · cited by 3Cardinal.beth_strictMonoStrictMono.iterate · cited by 3StrictMono.iterateStrictMono.mul_const · cited by 2StrictMono.mul_constCardinal.IsInaccessible.aleph_ord · cited by 2IsInaccessible.aleph_ordReal.strictMono_rpow_of_base_gt_one · cited by 2Real.strictMono_rpow_of_b…WithBot.strictMono_iff · cited by 2WithBot.strictMono_iffStrictMono.const_mul · cited by 2StrictMono.const_mulPreorder · cited by 7952PreorderStrictMono · cited by 706StrictMonoStrictMono.compCITED 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 by36

Results whose statement or proof uses this declaration.