Mathlib Changelog
v4
Changelog
About
Github
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