Theorems · Definition · order theory
OrderHom.const
(α : Type u_6) → [inst : Preorder α] → {β : Type u_7} → [inst_1 : Preorder β] → β →o α →o βConstant function bundled as an OrderHom.
- Defined in
- Mathlib.Order.Hom.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by13
Results whose statement or proof uses this declaration.
- SSet.stdSimplex.constproof · cited by 8
- OrderHom.prevFixedproof · cited by 4
- OrderHom.nextFixedproof · cited by 4
- OrderHom.nextFixed_leproof · cited by 2
- OmegaCompletePartialOrder.ContinuousHom.constproof · cited by 1
- OrderHom.gfp_const_inf_lestatement and proof · cited by 1
- OrderHom.comp_conststatement · cited by 0
- OrderHom.const_coe_coestatement and proof · cited by 0
- OrderHom.const_compstatement · cited by 0
- SSet.Augmented.StandardSimplex.extraDegeneracyproof · cited by 0
- OrderHom.bot_defstatement · cited by 0
- SSet.stdSimplex.const_down_toOrderHomstatement · cited by 0