Commit 2026-03-05 12:34 90795a09

View on Github →

feat(Combinatorics/SimpleGraphs): generalize SimpleGraph.map to any function (#36130) The point is to be able to use map to define graph contractions. Added the injectivity assumption where needed.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

modified theorem SimpleGraph.cliqueFinset_map_of_equiv

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.map_adj'

modified theorem SimpleGraph.map_id

modified theorem SimpleGraph.map_map

modified theorem SimpleGraph.map_monotone

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean