Commit 2024-11-12 10:38 e9be6572

View on Github →

feat(Combinatorics/SimpleGraph/Clique): add clique number (#18446) add clique number, maximal and maximum cliques, and theorems about the relationship between clique number and the cardinality of cliques.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.IsClique.card_le_cliqueNum

added theorem SimpleGraph.IsMaximumClique.isMaximalClique

added structure SimpleGraph.IsMaximumClique

added theorem SimpleGraph.exists_isNClique_cliqueNum

added theorem SimpleGraph.isMaximalClique_iff

added theorem SimpleGraph.isMaximumClique_iff

added theorem SimpleGraph.maximumClique_card_eq_cliqueNum

added theorem SimpleGraph.maximumClique_exists