Mathlib Map

Theorems · Theorem · order theory

OrderHom.id_coe

∀ {α : Type u_2} [inst : Preorder α], ⇑OrderHom.id = id
Defined in
Mathlib.Order.Hom.Basic
Cited by
14 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SimplexCategory.const_eq_id · cited by 6SimplexCategory.const_eq_…SimplexCategory.σ₀Iter_zero · cited by 5SimplexCategory.σ₀Iter_ze…SSet.unique_nonDegenerate_map · cited by 3SSet.unique_nonDegenerate…IsDedekindDomain.idealFactorsFunOfQuotHom_id · cited by 1IsDedekindDomain.idealFac…SSet.stdSimplex.notMem_boundary · cited by 1stdSimplex.notMem_boundarySSet.prodStdSimplex.nonDegenerate_max_dim_iff · cited by 1prodStdSimplex.nonDegener…OrderHom.eq_id_of_injective · cited by 1OrderHom.eq_id_of_injecti…LinOrd.id_apply · cited by 0LinOrd.id_applySimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible · cited by 0SimplexCategoryGenRel.sim…OmegaCompletePartialOrder.Chain.map_id · cited by 0Chain.map_idSimplexCategory.II.map'_id · cited by 0II.map'_idPreord.id_apply · cited by 0Preord.id_applyPartOrd.id_apply · cited by 0PartOrd.id_applyCategoryTheory.SimplicialThickening.functor_id · cited by 0SimplicialThickening.func…DFunLike.coe · cited by 62936DFunLike.coePreorder · cited by 7952PreorderOrderHom · cited by 934OrderHomOrderHom.id · cited by 37OrderHom.idOrderHom.id_coeCITED BYCITES

Cites4

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

Cited by14

Results whose statement or proof uses this declaration.