Mathlib Map

Theorems · Definition · order theory

OrderHom.toFun

{α : Type u_6} → {β : Type u_7} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → α → β

The underlying function of an OrderHom.

Defined in
Mathlib.Order.Hom.Basic
Cited by
45 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
PreorderPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ClosureOperator.isClosed_iff · cited by 14ClosureOperator.isClosed_…CategoryTheory.Limits.FormalCoproduct.cech · cited by 13FormalCoproduct.cechSimplexCategory.len_le_of_epi · cited by 9SimplexCategory.len_le_of…EsakiaHom.comp · cited by 9EsakiaHom.compPseudoEpimorphism.comp · cited by 9PseudoEpimorphism.compOrderHom.monotone' · cited by 8OrderHom.monotone'SimplexCategory.len_le_of_mono · cited by 8SimplexCategory.len_le_of…OrderMonoidHom.inlₗ · cited by 6OrderMonoidHom.inlₗOrderMonoidHom.inrₗ · cited by 5OrderMonoidHom.inrₗOrderAddMonoidHom.inlₗ · cited by 4OrderAddMonoidHom.inlₗOrderAddMonoidHom.inrₗ · cited by 3OrderAddMonoidHom.inrₗHahnSeries.embDomainOrderAddMonoidHom · cited by 3HahnSeries.embDomainOrder…SimplexCategory.isIso_of_bijective · cited by 2SimplexCategory.isIso_of_…ClosureOperator.mk.inj · cited by 1mk.injClosureOperator.mk.noConfusion · cited by 1mk.noConfusionPreorder · cited by 7952PreorderOrderHom · cited by 934OrderHomOrderHom.toFunCITED 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
  • OrderHomstatement and proof · cited by 934

Cited by91

Results whose statement or proof uses this declaration.