Theorem SSet.Subcomplex.Pairing.isUniquelyCodimOneFace

Modification history

2025-10-29 00:03
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean
feat(AlgebraicTopology/SimplicialSet): pairings of non degenerate simplices, following Sean Moss (#28332) …
Added SSet.Subcomplex.Pairing.isUniquelyCodimOneFaceView on Github →