Commit 2024-01-13 20:57 ba19db4d

View on Github →

feat: local graph operations (#9267)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

deleted theorem SimpleGraph.cliqueFree_of_replaceVertex_cliqueFree

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

added def SimpleGraph.addEdge

added theorem SimpleGraph.addEdge_of_adj

added theorem SimpleGraph.addEdge_self

added theorem SimpleGraph.card_edgeFinset_addEdge

added theorem SimpleGraph.card_edgeFinset_replaceVertex_of_adj

added theorem SimpleGraph.card_edgeFinset_replaceVertex_of_not_adj

added theorem SimpleGraph.disjoint_sdiff_neighborFinset_image

added theorem SimpleGraph.edgeFinset_addEdge

added theorem SimpleGraph.edgeFinset_replaceVertex_of_adj

added theorem SimpleGraph.edgeFinset_replaceVertex_of_not_adj

added theorem SimpleGraph.edgeSet_replaceVertex_of_adj

added theorem SimpleGraph.edgeSet_replaceVertex_of_not_adj

modified theorem SimpleGraph.not_adj_replaceVertex_same

added def SimpleGraph.replaceVertex

modified theorem SimpleGraph.replaceVertex_self