Theorem PartialOrder.mem_nerve_nonDegenerate_iff_injective

Modification history

2025-09-09 19:57
Mathlib/AlgebraicTopology/SimplicialSet/NerveNondegenerate.lean
feat(AlgebraicTopology): nondegenerate simplices in the nerve of a partially ordered type (#28337) …
Added PartialOrder.mem_nerve_nonDegenerate_iff_injectiveView on Github →