Theorems · Inductive type · order theory
OrderHom
(α : Type u_6) → (β : Type u_7) → [Preorder α] → [Preorder β] → Type (max u_6 u_7)
Bundled monotone (aka, increasing) function
- Defined in
- Mathlib.Order.Hom.Basic
- Cited by
- 934 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement · cited by 7,952
Cited by1,170
Results whose statement or proof uses this declaration.
- SignType.signstatement · cited by 128
- SimplexCategory.Hom.toOrderHomstatement · cited by 111
- Module.End.genEigenspacestatement · cited by 70
- OrderHom.monotonestatement and proof · cited by 70
- partialSupsstatement · cited by 67
- OrderHom.compstatement and proof · cited by 61
- OrderHom.extstatement and proof · cited by 55
- sign_posstatement · cited by 49
- OrderHom.dualstatement and proof · cited by 48
- OrderHom.toFunstatement and proof · cited by 45
- OrderHomClass.toOrderHomstatement · cited by 44
- OmegaCompletePartialOrder.Chain.mapstatement and proof · cited by 41
Showing the 200 most cited of 1,170.