Mathlib Map

Theorems · Definition · category theory

SimplexCategoryGenRel.mk

ℕ → SimplexCategoryGenRel

SimplexCategoryGenRel.mk is the main constructor for objects of SimplexCategoryGenRel.

Defined in
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Cited by
39 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SimplexCategoryGenRel.σ · cited by 26SimplexCategoryGenRel.σSimplexCategoryGenRel.δ · cited by 20SimplexCategoryGenRel.δSimplexCategoryGenRel.standardσ · cited by 10SimplexCategoryGenRel.sta…SimplexCategoryGenRel.faces.casesOn · cited by 5faces.casesOnSimplexCategoryGenRel.degeneracies.casesOn · cited by 4degeneracies.casesOnSimplexCategoryGenRel.standardσ_comp_standardσ · cited by 2SimplexCategoryGenRel.sta…SimplexCategoryGenRel.δ_comp_δ · cited by 2SimplexCategoryGenRel.δ_c…SimplexCategoryGenRel.σ_comp_σ · cited by 2SimplexCategoryGenRel.σ_c…SimplexCategoryGenRel.standardσ.congr_simp · cited by 2standardσ.congr_simpSimplexCategoryGenRel.ext · cited by 1SimplexCategoryGenRel.extSimplexCategoryGenRel.hom_induction · cited by 1SimplexCategoryGenRel.hom…SimplexCategoryGenRel.rec · cited by 1SimplexCategoryGenRel.recSimplexCategoryGenRel.P_δ.δ · cited by 1P_δ.δSimplexCategoryGenRel.P_σ.σ · cited by 1P_σ.σSimplexCategoryGenRel.generators.δ · cited by 1generators.δPrefunctor.obj · cited by 1241Prefunctor.objSimplexCategoryGenRel · cited by 39SimplexCategoryGenRelCategoryTheory.Paths.of · cited by 20Paths.ofFreeSimplexQuiver · cited by 2FreeSimplexQuiverSimplexCategoryGenRel.mkCITED BYCITES

Cites4

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

Cited by49

Results whose statement or proof uses this declaration.