Theorems · Theorem · category theory

AugmentedSimplexCategory.eqToHom_toOrderHom

∀ {x y : SimplexCategory} (h : CategoryTheory.WithInitial.of x = CategoryTheory.WithInitial.of y),
  SimplexCategory.Hom.toOrderHom (CategoryTheory.WithInitial.down (CategoryTheory.eqToHom h)) =
    (Fin.castOrderIso ⋯).toOrderEmbedding.toOrderHom

Defined in: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Cited by: 3 results in Mathlib
Foundations: Depth 36 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

SimplexCategorystatement and proof · cited by 2,204
OrderHomstatement · cited by 934
CategoryTheory.eqToHomstatement · cited by 860
SimplexCategory.lenstatement · cited by 542
CategoryTheory.WithInitialstatement · cited by 144
SimplexCategory.Hom.toOrderHomstatement · cited by 111
CategoryTheory.WithInitial.downstatement · cited by 27
OrderIso.toOrderEmbeddingstatement · cited by 22
OrderEmbedding.toOrderHomstatement · cited by 16
Fin.castOrderIsostatement · cited by 11
SimplexCategory.eqToHom_toOrderHomproof · cited by 5
CategoryTheory.WithInitial.of.noConfusionproof · cited by 2

Cited by3

Results whose statement or proof uses this declaration.

AugmentedSimplexCategory.inr_comp_associatorproof · cited by 1
AugmentedSimplexCategory.inl_comp_inl_comp_associatorproof · cited by 1
AugmentedSimplexCategory.inr_comp_inl_comp_associatorproof · cited by 1