Mathlib Map

Theorems · Definition · order theory

CategoryTheory.homOfLE

{X : Type u} → [inst : Preorder X] → {x y : X} → x ≤ y → (x ⟶ y)

Express an inequality as a morphism in the corresponding preorder category.

Defined in
Mathlib.CategoryTheory.Category.Preorder
Cited by
554 results in Mathlib
Foundations
Depth 11 from the axioms, rests on 53 definitions · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AlgebraicGeometry.Scheme.Hom.appLE · cited by 138Hom.appLECategoryTheory.ComposableArrows.map' · cited by 133ComposableArrows.map'Monotone.functor · cited by 66Monotone.functorCategoryTheory.Triangulated.TStructure.eTruncLTι · cited by 36TStructure.eTruncLTιCategoryTheory.ComposableArrows.naturality' · cited by 31ComposableArrows.naturali…LE.le.hom · cited by 30le.homAlgebraicGeometry.Scheme.Hom.appLE_map · cited by 27Hom.appLE_mapTopCat.Presheaf.restrictOpen · cited by 25Presheaf.restrictOpenCategoryTheory.Triangulated.TStructure.eTruncGEπ · cited by 25TStructure.eTruncGEπAlgebraicGeometry.Scheme.Hom.map_appLE · cited by 24Hom.map_appLECategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀' · cited by 23SpectralObject.mapFourδ₁T…CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃' · cited by 23SpectralObject.mapFourδ₄T…CompleteLattice.MulticoequalizerDiagram.multispanIndex · cited by 20MulticoequalizerDiagram.m…CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX · cited by 19SpectralSequence.pageXAlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen · cited by 18IsAffineOpen.isLocalizati…Quiver.Hom · cited by 32603Quiver.HomPreorder · cited by 7952PreorderCategoryTheory.homOfLECITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by706

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 706.