[Merged by Bors] - feat(Combinatorics/Graph): infimum

[Jun2M]

Adds Mathlib/Combinatorics/Graph/Lattice.lean, which defines intersections, as Inf, of Graph α β values and proves the lattice structure induced by binary intersection.

Main additions

• SemilatticeInf (Graph α β)

Co-authored-by: Peter Nelson apn.uni@gmail.com

---

[github-actions]

PR summary f3dd886f91

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.Graph.Lattice (new file)	493

---

Declarations diff

+ Compatible.edgeSet_inf
+ disjoint_iff
+ edgeSet_inf
+ inf_inc_iff
+ inf_isLink
+ inf_isLoopAt_iff
+ inf_isNonloopAt_iff
+ instance : SemilatticeInf (Graph α β)
+ vertexSet_inf

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[vihdzp]

I think what you instead want to prove is that graphs are a complete lattice, similar to how it's done for simple graphs.

[Jun2M]

It would be marvelous if Graph forms a complete lattice. However, due to compatibility issue, this is not true: Consider two path graphs of length 1, uev & xey where e is the only edge in both graphs. What is the union of the two graphs? As Graph is not a hypergraph, e must be incident to at most 2 vertices yet the first graph would suggest it should be incident to u and v whlie the second graph would disagree and suggest that it should be incident to x and y.

It is true that if you consider 1. all subgraphs of a particular graph or 2. WithTop (Graph α β), then they form CompleteLattice. I have proof for both of them but as they are talking about a different type, I thought I should add it to another file in a later PR.

[vihdzp]

I think what you're describing is a ConditionallyCompletePartialOrder?

[Jun2M]

Thank you! I didn't know about this one. I have just proved that Graph is indeed ConditionallyCompletePartialOrder. However, it required using ⊥, the empty graph, as the error value which is in PR #37610 not yet merged. If I understand correctly, this is orthogonal to SemilatticeInf instance so I will leave it as is and add ConditionallyCompletePartialOrder to a later PR that depends on this PR and #37610.

[vihdzp]

Likewise elsewhere.

Suggested change

	lemma sInf_isLink (Gs : Set (Graph α β)) [Decidable Gs.Nonempty] :
	lemma isLink_sInf (Gs : Set (Graph α β)) [Decidable Gs.Nonempty] :

[Jun2M]

This came up in #35879 and isLink was merged as a postfix at the end. @YaelDillies?

[YaelDillies]

I already expressed my preference that isLink should be a prefix, and Bhavik's that it should be a postfix

[Jun2M]

I have removed the sInf related things as order theory PRs has to be merged first for that. With just SemilatticeInf, this PR should be fine to be merged. In the future, I will add the instance for sInf once Mathlib has the right class.

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[b-mehta]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step