Commit 2023-10-14 07:05 6c63dfbe

View on Github →

feat: vertex replacement (#6808) cliqueFree_of_replaceVertex_cliqueFree is still quite long.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.adj_replaceVertex_iff_of_ne

added theorem SimpleGraph.adj_replaceVertex_iff_of_ne_left

added theorem SimpleGraph.adj_replaceVertex_iff_of_ne_right

added theorem SimpleGraph.not_adj_replaceVertex_same

added theorem SimpleGraph.replaceVertex_self

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.cliqueFree_of_replaceVertex_cliqueFree