[Merged by Bors] - feat(Combinatorics/SimpleGraph/Clique): add clique number by ooovi · Pull Request #18446 · leanprover-community/mathlib4

ooovi · 2024-10-30T16:00:46Z

add clique number, maximal and maximum cliques, and theorems about the relationship between clique number and the cardinality of cliques.

github-actions · 2024-10-30T16:01:36Z

PR summary cc625ef21f

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Clique	562	570	+8 (+1.42%)

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.SimpleGraph.Triangle.Counting` `Mathlib.Combinatorics.SimpleGraph.Turan`	6
`Mathlib.Combinatorics.SimpleGraph.Triangle.Basic` `Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite`	7
`Mathlib.Combinatorics.SimpleGraph.Clique`	8

Declarations diff

+ IsClique.card_le_cliqueNum
+ IsMaximumClique
+ IsMaximumClique.isMaximalClique
+ cliqueNum
+ exists_isNClique_cliqueNum
+ isMaximalClique_iff
+ isMaximumClique_iff
+ maximumClique_card_eq_cliqueNum
+ maximumClique_exists

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

FordUniver · 2024-11-01T09:23:56Z

@YaelDillies @kmill We are now defining IsMaximumClique and IsMaximalClique as structures, following IsNClique. Two things were unclear to me: why / when is the I at the beginning capitalized? Is it upper case for structures and lower case for lemmas? And why do we go for (s : Finset α) (smc : G.IsMaximumClique s) rather than (s : G.MaximumClique), i.e., why don't we redefine the structures to have the set as an attribute rather than an argument?

Besides that, is there anything this PR is missing in terms of fundamental statements that you can think of?

Mathlib/Combinatorics/SimpleGraph/Clique.lean

YaelDillies · 2024-11-02T14:47:03Z

Mathlib/Combinatorics/SimpleGraph/Clique.lean

+/-- A maximal clique in a graph `G` is a clique that cannot be extended by adding more vertices. -/
+structure IsMaximalClique (G : SimpleGraph α) (s : Finset α) : Prop where
+  (clique : G.IsClique s)
+  (maximal : ∀ t : Finset α, G.IsClique t → s ⊆ t → t = s)


What is the use case of these predicates?

You mean why define maximal cliques? Seemed sensible to include it when defining maximum cliques, but I don't think we need it for our particular application right now (unless @ooovi disagrees).

I mean both maximal and maximum cliques

Right now @ooovi was working on the AM-GM proof of Mantel which needs this notion. We have also in the past needed the clique number when doing some auxiliary stuff for the hypercube / sensitivity conjecture and I want to clean that up as well.

Actually both of these need the independence number (which requires a notion of independence set in the first place), for which we are preparing another PR that's intended to build on this.

Right now @ooovi was working on the AM-GM proof of Mantel which needs this notion. We have also in the past needed the clique number when doing some auxiliary stuff for the hypercube / sensitivity conjecture and I want to clean that up as well.

How much do you need it? Is it like one lemma or two, or do you a full API about them

For my specific proof, I need the dual of lemma maximumClique_card_eq_cliqueNum (s : Finset α) (sm : G.IsMaximumClique s) : #s = G.cliqueNum and lemma maximumClique_exists : ∃ (s : Finset α), G.IsMaximumClique s, which are the corresponding statements about maximum independent sets and the coclique number. The dualization is in a seperate PR, #18608.

Mathlib/Combinatorics/SimpleGraph/Clique.lean

YaelDillies

I have strain injuries to both wrists, hence must not type much. Please apologise the poor spelling, vague indications and general conciseness.

FordUniver · 2024-11-02T22:52:38Z

I have strain injuries to both wrists, hence must not type much. Please apologise the poor spelling, vague indications and general conciseness.

Thanks for the review and get better!

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Mathlib/Combinatorics/SimpleGraph/Clique.lean

b-mehta

This is looking in pretty good shape!

Mathlib/Combinatorics/SimpleGraph/Clique.lean

b-mehta

Thanks!

bors d+

Mathlib/Combinatorics/SimpleGraph/Clique.lean

mathlib-bors · 2024-11-12T09:49:15Z

✌️ ooovi can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

ooovi · 2024-11-12T10:05:23Z

bors r+

mathlib-bors · 2024-11-12T10:05:26Z

Already running a review

ooovi · 2024-11-12T10:06:15Z

bors merge

add clique number, maximal and maximum cliques, and theorems about the relationship between clique number and the cardinality of cliques. Co-authored-by: Christoph Spiegel <christophspiegel.berlin@gmail.comm> Co-authored-by: FordUniver <61389961+FordUniver@users.noreply.github.com> Co-authored-by: ooovi <79147175+ooovi@users.noreply.github.com>

mathlib-bors · 2024-11-12T10:47:05Z

Pull request successfully merged into master.

Build succeeded:

Followup to #18446

add clique number, maximal and maximum cliques, and theorems about the relationship between clique number and the cardinality of cliques. Co-authored-by: Christoph Spiegel <christophspiegel.berlin@gmail.comm> Co-authored-by: FordUniver <61389961+FordUniver@users.noreply.github.com> Co-authored-by: ooovi <79147175+ooovi@users.noreply.github.com>

Followup to #18446

add clique number, maximal and maximum cliques, and theorems about the relationship between clique number and the cardinality of cliques. Co-authored-by: Christoph Spiegel <christophspiegel.berlin@gmail.comm> Co-authored-by: FordUniver <61389961+FordUniver@users.noreply.github.com> Co-authored-by: ooovi <79147175+ooovi@users.noreply.github.com>

Followup to #18446

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Oct 30, 2024

github-actions bot added the t-combinatorics Combinatorics label Oct 30, 2024

ooovi marked this pull request as ready for review October 30, 2024 17:38

ooovi requested a review from YaelDillies October 30, 2024 17:39

FordUniver requested a review from kmill November 1, 2024 09:33

YaelDillies reviewed Nov 2, 2024

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 2, 2024

ooovi mentioned this pull request Nov 4, 2024

[Merged by Bors] - feat(Combinatorics/SimpleGraph): add independent sets #18608

Closed

1 task

ooovi and others added 16 commits November 5, 2024 08:51

adding cliqueNum and some theorems

3756fe3

docs, soothing linter

1ff3c3f

some cleanup

e0ec518

add lemma connecting maximal and maximum cliques

4cea7c5

added a theorem on existence of a maximum clique

1f94886

rewrite maximalClique_of_maximumClique to use push_neg

ff069e3

saved one line

a0d3ad5

redefined Max* cliques through structures

5ffb4f3

removed commented out code

3e66b56

Update Mathlib/Combinatorics/SimpleGraph/Clique.lean

eeb8fed

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

removed superfluous fin :

6605f1d

turned structures propositional

a95185a

turned instances of prop structures to lemmas

f68c004

removed superfluous (?) Nonempty

ce73fd2

split up finite results into Finset of cliques

7a599e9

removed TODO comment

d2a7378

replace clique with IsClique in IsNClique

54670c5

YaelDillies reviewed Nov 6, 2024

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Clique.lean Outdated Show resolved Hide resolved

fixed doc string

f94b691

YaelDillies requested a review from b-mehta November 10, 2024 10:02

b-mehta reviewed Nov 10, 2024

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Clique.lean Outdated Show resolved Hide resolved

b-mehta reviewed Nov 10, 2024

View reviewed changes

ooovi and others added 3 commits November 11, 2024 09:35

incorporating pr comments

42e3660

rewriting IsMaximalClique as Maximal G.IsClique

7612312

minor changes

2c256da

b-mehta approved these changes Nov 12, 2024

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Nov 12, 2024

Apply suggestions from code review

cc625ef

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

ooovi closed this Nov 12, 2024

ooovi reopened this Nov 12, 2024

mathlib-bors bot changed the title ~~feat(Combinatorics/SimpleGraph/Clique): add clique number~~ [Merged by Bors] - feat(Combinatorics/SimpleGraph/Clique): add clique number Nov 12, 2024

mathlib-bors bot closed this Nov 12, 2024

mathlib-bors bot deleted the feat-clique-number branch November 12, 2024 10:47

Ruben-VandeVelde mentioned this pull request Nov 12, 2024

[Merged by Bors] - chore: fix the name of the IsNClique.isClique field #18908

Closed

mathlib-bors bot pushed a commit that referenced this pull request Nov 12, 2024

chore: fix the name of the IsNClique.isClique field (#18908)

bb31b35

Followup to #18446

Jun2M pushed a commit that referenced this pull request Nov 17, 2024

chore: fix the name of the IsNClique.isClique field (#18908)

0c1ba9d

Followup to #18446

TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024

chore: fix the name of the IsNClique.isClique field (#18908)

86ed94f

Followup to #18446

SnirBroshi mentioned this pull request Feb 11, 2026

Graph theory def: Maximal/maximum cliques & independent sets #34962

Open

Conversation

ooovi commented Oct 30, 2024

Uh oh!

github-actions bot commented Oct 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary cc625ef21f

Import changes for modified files

Declarations diff

Uh oh!

FordUniver commented Nov 1, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies Nov 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

FordUniver Nov 2, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Nov 3, 2024

Choose a reason for hiding this comment

Uh oh!

FordUniver Nov 3, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Nov 6, 2024

Choose a reason for hiding this comment

Uh oh!

ooovi Nov 6, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

FordUniver commented Nov 2, 2024

Uh oh!

Uh oh!

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Nov 12, 2024

Uh oh!

ooovi commented Nov 12, 2024

Uh oh!

mathlib-bors bot commented Nov 12, 2024

Uh oh!

ooovi commented Nov 12, 2024

Uh oh!

mathlib-bors bot commented Nov 12, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented Oct 30, 2024 •

edited

Loading

YaelDillies Nov 2, 2024 •

edited

Loading

ooovi Nov 6, 2024 •

edited

Loading