feat(Combinatorics/Graph): Add Graph intersection operations

[Jun2M]

Adds Mathlib/Combinatorics/Graph/InterUnion.lean, which defines intersections of Graph α β values and proves the lattice structure induced by binary intersection. Following PR will add the union operations to this file.

Main additions

• Graph.iInter: intersection of a nonempty indexed family of graphs. Vertices are the intersection of vertex sets; an edge is kept iff it is a link in every graph with a common pair of endpoints (pairwise compatibility is assumed where needed).
• Graph.sInter: Infimum of a nonempty Set (Graph α β), defined via iInter on the subtype.
• Graph.inter: Binary intersection. Vertices are V(G) ∩ V(H). Edges are those in both edge sets on which G and H agree on IsLink for all endpoint pairs; IsLink on the intersection is conjunction of the two IsLink predicates.
• Proof of SemilatticeInf (Graph α β)

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

---

[github-actions]

PR summary 8f1377de1f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.Graph.InterUnion (new file)	504

---

Declarations diff

+ iInter
+ iInter_le
+ instance : Inter (Graph α β) where inter := Graph.inter
+ instance : SemilatticeInf (Graph α β)
+ instance : Std.Associative (α := Graph α β) (· ∩ ·)
+ instance : Std.Commutative (α := Graph α β) (· ∩ ·)
+ inter
+ inter_assoc
+ inter_comm
+ inter_edgeSet
+ inter_isLink_iff
+ inter_le_left
+ inter_le_right
+ inter_vertexSet
+ le_iInter_iff
+ le_inter
+ le_sInter_iff
+ sInter
+ sInter_le

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.