Theorem SimplexCategoryGenRel.isAdmissible_of_isChain_of_forall_getElem_le

Modification history

2025-10-17 12:35
Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
fix: Improve definition of `SimplexCategoryGenRel.IsAdmissible` (#30586) …
Added SimplexCategoryGenRel.isAdmissible_of_isChain_of_forall_getElem_leView on Github →