Commit 2025-03-10 17:36 688aba31

View on Github →

feat: a graph with finitely many vertices has finitely many subgraphs (#22630) From LeanCamCombi

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem SimpleGraph.Subgraph.edgeSet_map

Modified Mathlib/Data/Sym/Sym2.lean

added theorem Sym2.fromRel_relationMap

Modified Mathlib/Logic/Relation.lean

added theorem Relation.map_symmetric