Theorems · Theorem · order theory
OrderHom.monotone
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), Monotone ⇑f- Defined in
- Mathlib.Order.Hom.Basic
- Cited by
- 70 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Preorderstatement and proof · cited by 7,952
- Monotonestatement · cited by 1,397
- OrderHomstatement and proof · cited by 934
- OrderHom.monotone'proof · cited by 8
Cited by89
Results whose statement or proof uses this declaration.
- OrderHom.monoproof · cited by 28
- CategoryTheory.Functor.WellOrderInductionData.liftstatement · cited by 7
- Module.End.mem_genEigenspaceproof · cited by 4
- Module.End.mem_genEigenspace_natproof · cited by 4
- CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHomstatement · cited by 4
- SimplexCategory.eq_σ_comp_of_not_injectiveproof · cited by 4
- OrderHom.toFunctorproof · cited by 4
- FirstOrder.Language.DirectLimit.Equiv_iSupstatement · cited by 4
- Part.Fix.approx_mono'proof · cited by 4
- SSet.stdSimplex.monotone_applyproof · cited by 4
- OrderHom.uliftRightMapproof · cited by 3
- SSet.unique_nonDegenerate_mapproof · cited by 3