Commit 2025-08-25 23:08 bd6f86a7

View on Github →

feat(Combinatorics/SimpleGraph): card_edgeFinset_map (#28446)

Estimated changes

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

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.Iso.card_edgeFinset_eq

added theorem SimpleGraph.card_edgeFinset_map

added theorem SimpleGraph.edgeFinset_map

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.edgeSet_map

added theorem SimpleGraph.support_map

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

deleted theorem SimpleGraph.Iso.card_edgeFinset_eq