feat(Combinatorics/Graph): Edge cut of Graph

[Jun2M]

This PR introduces

• edgeCut: A function on set of vertices that returns the set of edges with exactly one end in the set.
• IsEdgeCut: A predicate for set of edges that promises it is edgeCut of some set.
• IsBridge: An edge e is a bridge iff it is a singleton edge cut.
• IsBond: An edge Set B is bond iff it is minimal nonempty edge cut.

---

• depends on: [Merged by Bors] - feat(Combinatorics/Graph): graph deletion operations #35879

[github-actions]

PR summary 2a556ee342

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsBond
+ IsBond.isBridge
+ IsBond.isEdgeCut
+ IsBond.nonempty
+ IsBond.of_isClosedSubgraph
+ IsBond.subset
+ IsBridge
+ IsBridge.anti_of_mem
+ IsBridge.isBond
+ IsBridge.isEdgeCut
+ IsBridge.mem_edgeSet
+ IsBridge.of_isClosedSubgraph
+ IsClosedSubgraph.edgeCut_subset
+ IsClosedSubgraph.isBond
+ IsClosedSubgraph.isBridge_iff
+ IsClosedSubgraph.isEdgeCut
+ IsEdgeCut
+ IsEdgeCut.anti
+ IsEdgeCut.exists
+ IsEdgeCut.exists_of_isLink
+ IsEdgeCut.of_isClosedSubgraph
+ IsEdgeCut.subset
+ IsEdgeCut.symmDiff
+ IsLink.mem_edgeCut_iff
+ IsSubgraph.edgeCut_eq_inter
+ IsSubgraph.isLink_iff'
+ edgeCut
+ edgeCut_eq_empty_iff
+ edgeCut_subset
+ edgeCut_symmDiff
+ edgeCut_vertexSet_diff
+ mem_edgeCut_iff

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).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Combinatorics/Graph): graph deletion operations #35879
  By Dependent Issues (🤖). Happy coding!