Commit 2024-01-24 02:24 6219c283

View on Github →

feat: transfer of graph properties over maps (#9708) Part of #9317.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.CliqueFree.comap

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.Iso.card_edgeFinset_eq

added theorem SimpleGraph.Iso.card_eq

deleted theorem SimpleGraph.Iso.card_eq_of_iso

added def SimpleGraph.overFin