Commit 2024-01-09 19:00 4fd6d057

View on Github →

chore(AlgebraicTopology/TopologicalSimplex): clean up, golf (#9431)

Estimated changes

Modified Mathlib/AlgebraicTopology/TopologicalSimplex.lean

modified def SimplexCategory.toTopMap

modified def SimplexCategory.toTopObj

Modified Mathlib/Data/Finset/Basic.lean

added theorem Set.pairwiseDisjoint_filter