Skip to content

[Merged by Bors] - feat(Combinatorics/SimpleGraph): define CompleteEquipartiteSubgraph#27599

Closed
mitchell-horner wants to merge 38 commits intoleanprover-community:masterfrom
mitchell-horner:complete-equipartite-subgraph
Closed

[Merged by Bors] - feat(Combinatorics/SimpleGraph): define CompleteEquipartiteSubgraph#27599
mitchell-horner wants to merge 38 commits intoleanprover-community:masterfrom
mitchell-horner:complete-equipartite-subgraph

Conversation

@mitchell-horner
Copy link
Copy Markdown
Collaborator

@mitchell-horner mitchell-horner commented Jul 28, 2025 •
edited by YaelDillies
Loading

Define the complete equipartite subgraphs in r parts each of size t in G as the r subsets of vertices each of size t such that vertices in distinct subsets are adjacent.

In this case Nonempty (G.CompleteEquipartiteSubgraph r t) is equivalent to completeEquipartiteGraph r t ⊑ G, that is, finding r subsets of vertices each of size t in G such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from completeEquipartiteGraph r t to G.

Open in Gitpod

@github-actions github-actions bot added large-import Automatically added label for PRs with a significant increase in transitive imports t-combinatorics Combinatorics labels Jul 28, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 28, 2025 •
edited
Loading

PR summary 8f07524533

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ CompleteEquipartiteSubgraph
+ card_verts
+ completeEquipartiteGraph_isContained_iff
+ completeEquipartiteGraph_succ_isContained_iff
+ disjoint
+ nonempty_of_eq_zero_or_eq_zero
+ ofCopy
+ toCopy
+ verts
+ verts_eq_biUnion

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 scripts/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 28, 2025
@mitchell-horner mitchell-horner mentioned this pull request Aug 13, 2025
Closed
@mitchell-horner mitchell-horner mentioned this pull request Aug 20, 2025
Open
7 tasks
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 20, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Aug 20, 2025

This pull request has conflicts, please merge master and resolve them.

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 20, 2025
@github-actions github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Aug 25, 2025
YaelDillies
YaelDillies reviewed Sep 3, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's your use case?

Comment thread Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean Outdated
Comment thread Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean Outdated
Comment thread Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean Outdated
Comment thread Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean Outdated
Comment thread Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean Outdated
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 3, 2025
@mitchell-horner
Copy link
Copy Markdown
Collaborator Author

mitchell-horner commented Sep 3, 2025 •
edited
Loading

What's your use case?

@YaelDillies This definition fell out of golfing #28685 and is similar in concept to #27602. These are the lines that use the definition in that PR.

Having this representation allows me to make the handwavy argument I might do on pen-and-paper that "to prove $K_r (t) \sqsubseteq G$ it suffices to show that $G$ contains $r$ subsets of vertices of equal size $t$ such that...", in one line!

@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Sep 3, 2025

Having this representation allows me to make the handwavy argument I might do on pen-and-paper that "to prove $K_r (t) \sqsubseteq G$ it suffices to show that $G$ contains $r$ subsets of vertices of equal size $t$ such that...", in one line!

But why can't you do this without the structure, by eg simply stating completeEquipartiteGraph r t ⊑ G ↔ ∃ parts : Fin r → Set V, ...?

@mitchell-horner
Copy link
Copy Markdown
Collaborator Author

mitchell-horner commented Sep 3, 2025 •
edited
Loading

But why can't you do this without the structure, by eg simply stating completeEquipartiteGraph r t ⊑ G ↔ ∃ parts : Fin r → Set V, ...?

Of course I can write that statement without the structure; the structure is for convenience and readability in subsequent statements and proofs.

Compare these snippets:

  ∃ (parts : Fin (n + 1) → Finset V), (∀ ⦃i⦄, #(parts i) = t)
      ∧ (∀ ⦃i₁ i₂⦄, i₁ ≠ i₂ → ∀ v ∈ parts i₁, ∀ w ∈ parts i₂, G.Adj v w)
  ↔ ∃ (parts : Fin n → Finset V)  (s : Finset V), #s = t ∧ (∀ ⦃i⦄, #(parts i) = t)
      ∧ (∀ ⦃i₁ i₂⦄, i₁ ≠ i₂ → ∀ v ∈ parts i₁, ∀ w ∈ parts i₂, G.Adj v w)
      ∧ ∀ v₁ ∈ s, ∀ i, ∀ v₂ ∈ A.parts i, G.Adj v₁ v₂ := sorry

  Nonempty (G.CompleteEquipartiteSubgraph (n + 1) t)
    ↔ ∃ (A : G.CompleteEquipartiteSubgraph n t) (s : Finset V),
        #s = t ∧ ∀ v₁ ∈ s, ∀ i, ∀ v₂ ∈ A.parts i, G.Adj v₁ v₂ := sorry

@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Sep 3, 2025

@b-mehta, what do you think?

@mitchell-horner mitchell-horner changed the title feat(Combinatorics/SimpleGraph): define completeEquipartiteSubgraph feat(Combinatorics/SimpleGraph): define CompleteEquipartiteSubgraph Sep 3, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 19, 2025

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Nov 19, 2025

It is very annoying to have to comment twice the same thing across two PRs. Could you maybe merge them together?

@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 26, 2025
@mitchell-horner
Copy link
Copy Markdown
Collaborator Author

mitchell-horner commented Dec 6, 2025 •
edited
Loading

It is very annoying to have to comment twice the same thing across two PRs. Could you maybe merge them together?

@YaelDillies In this case, the structure is far more important for convenience and readability in the use case that keeps track of multiple overlapping complete equipartite subgraphs.

(In the PR you are referring to, I could get away with completeBipartiteGraph_isContained_iff alone.)

The abbrev verts (defined via via disjiUnion using parts and isCompleteBetween from the structure) is also very convenient for statements like:

(G.between K.verts K.vertsᶜ).degree v < #K.verts - t' + t

I cannot play the same games on both PRs.

@mitchell-horner mitchell-horner removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 6, 2025
@YaelDillies YaelDillies requested a review from b-mehta December 7, 2025 14:28
b-mehta
b-mehta reviewed Dec 19, 2025
View reviewed changes
Comment thread Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean Outdated
Comment thread Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean Outdated
Comment thread Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean Outdated
@b-mehta b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 19, 2025
@mitchell-horner mitchell-horner removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 7, 2026
b-mehta
b-mehta reviewed Mar 1, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 1, 2026
@mitchell-horner
feat(Combinatorics/SimpleGraph): define CompleteEquipartiteSubgraph (…
3542f17 
…#27599)

Define the complete equipartite subgraphs in `r` parts each of size `t` in `G` as the `r` subsets of vertices each of size `t` such that vertices in distinct subsets are adjacent.

In this case `Nonempty (G.CompleteEquipartiteSubgraph r t)` is equivalent to `completeEquipartiteGraph r t ⊑ G`, that is, finding `r` subsets of vertices each of size `t` in `G` such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from `completeEquipartiteGraph r t` to `G`.
@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Mar 1, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 1, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Combinatorics/SimpleGraph): define CompleteEquipartiteSubgraph [Merged by Bors] - feat(Combinatorics/SimpleGraph): define CompleteEquipartiteSubgraph Mar 1, 2026
@mathlib-bors mathlib-bors bot closed this Mar 1, 2026
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Mar 2, 2026
@mitchell-horner @pfaffelh
feat(Combinatorics/SimpleGraph): define CompleteEquipartiteSubgraph (…
086c770 
…leanprover-community#27599)

Define the complete equipartite subgraphs in `r` parts each of size `t` in `G` as the `r` subsets of vertices each of size `t` such that vertices in distinct subsets are adjacent.

In this case `Nonempty (G.CompleteEquipartiteSubgraph r t)` is equivalent to `completeEquipartiteGraph r t ⊑ G`, that is, finding `r` subsets of vertices each of size `t` in `G` such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from `completeEquipartiteGraph r t` to `G`.
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026
@mitchell-horner @xroblot
feat(Combinatorics/SimpleGraph): define CompleteEquipartiteSubgraph (…
b0e89de 
…leanprover-community#27599)

Define the complete equipartite subgraphs in `r` parts each of size `t` in `G` as the `r` subsets of vertices each of size `t` such that vertices in distinct subsets are adjacent.

In this case `Nonempty (G.CompleteEquipartiteSubgraph r t)` is equivalent to `completeEquipartiteGraph r t ⊑ G`, that is, finding `r` subsets of vertices each of size `t` in `G` such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from `completeEquipartiteGraph r t` to `G`.
pevogam pushed a commit to pevogam/mathlib4 that referenced this pull request Mar 19, 2026
@mitchell-horner @pevogam
feat(Combinatorics/SimpleGraph): define CompleteEquipartiteSubgraph (…
52a0b95 
…leanprover-community#27599)

Define the complete equipartite subgraphs in `r` parts each of size `t` in `G` as the `r` subsets of vertices each of size `t` such that vertices in distinct subsets are adjacent.

In this case `Nonempty (G.CompleteEquipartiteSubgraph r t)` is equivalent to `completeEquipartiteGraph r t ⊑ G`, that is, finding `r` subsets of vertices each of size `t` in `G` such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from `completeEquipartiteGraph r t` to `G`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

@b-mehta b-mehta b-mehta left review comments

Assignees

@YaelDillies YaelDillies

Labels

ready-to-merge This PR has been sent to bors. t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@mitchell-horner @mathlib4-merge-conflict-bot @YaelDillies @mathlib4-dependent-issues-bot @b-mehta @jcommelin