Commit 2025-03-19 19:40 86e2e68c

View on Github →

feat(Combinatorics/SimpleGraph/Clique): add lemmas about cliques in G ⊔ edge v w (#22370) Add lemmas about cliques in a graph G versus cliques in G ⊔ edge v w. Refactor SimpleGraph.CliqueFree.sup_edge

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.CliqueFree.mem_of_sup_edge_isNClique

added theorem SimpleGraph.IsClique.sdiff_of_sup_edge

added theorem SimpleGraph.IsNClique.erase_of_sup_edge_of_mem

added theorem SimpleGraph.isClique_sup_edge_of_ne_iff

added theorem SimpleGraph.isClique_sup_edge_of_ne_sdiff