Commit 2025-01-11 18:54 e01427c6

View on Github →

feat(Combinatorics/SimpleGraph): add independent sets (#18608) dualize the clique API to obtain independent sets, prove theorems about the dual relationship to cliques, dualize and add some theorems.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added def SimpleGraph.IndepSetFree

added def SimpleGraph.IndepSetFreeOn

added theorem SimpleGraph.IsIndepSet.card_le_indepNum

added theorem SimpleGraph.IsIndepSet.nonempty_mem_compl_mem_edge

added theorem SimpleGraph.IsMaximumIndepSet.isMaximalIndepSet

added structure SimpleGraph.IsMaximumIndepSet

added structure SimpleGraph.IsNIndepSet

added theorem SimpleGraph.cliqueFree_compl

added theorem SimpleGraph.cliqueNum_compl

added theorem SimpleGraph.exists_isNIndepSet_indepNum

added theorem SimpleGraph.indepNum_compl

added def SimpleGraph.indepSetFinset

added theorem SimpleGraph.indepSetFree_compl

added def SimpleGraph.indepSetSet

added theorem SimpleGraph.isClique_compl

added theorem SimpleGraph.isIndepSet_compl

added theorem SimpleGraph.isIndepSet_iff

added theorem SimpleGraph.isIndepSet_neighborSet_of_triangleFree

added theorem SimpleGraph.isMaximalClique_compl

added theorem SimpleGraph.isMaximalIndepSet_compl

added theorem SimpleGraph.isMaximalIndepSet_iff

added theorem SimpleGraph.isMaximumClique_compl

added theorem SimpleGraph.isMaximumIndepSet_compl

added theorem SimpleGraph.isNClique_compl

added theorem SimpleGraph.isNIndepSet_compl

added theorem SimpleGraph.maximumIndepSet_card_eq_indepNum

added theorem SimpleGraph.maximumIndepSet_exists

added theorem SimpleGraph.mem_indepSetFinset_iff

added theorem SimpleGraph.mem_indepSetSet_iff