feat(Combinatorics): define directed hypergraphs

[espottesmith]

This PR defines directed hypergraphs:

@[ext]
structure DiHypergraph (α : Type*) where
  /-- The vertex set -/
  vertexSet : Set α
  /-- The edge set -/
  edgeSet : Set ((Set α) × (Set α))
  /-- Each edge is a pair (s, d), where s ⊆ vertexSet and d ⊆ vertexSet -/
  edge_src_dst_isSubset_vertexSet' : ∀ ⦃e⦄, e ∈ edgeSet → e.1 ⊆ vertexSet ∧ e.2 ⊆ vertexSet

Additional definitions:

• tail/head stars and negative/positive stars
• some special cases (B-Graph, F-Graph, BF-Graph, and what I'm calling a "non-endless" dihypergraph, where neither the source/tail nor the destination/head are empty)
• Vertex and (hyper)edge adjacency
• isolated vertices
• empty and nonempty dihypergraphs

The design employed here is based off of #28613, but this PR does not depend on that one.

---

[github-actions]

PR summary 79463c8311

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.DiHypergraph.Basic (new file)	742

---

Declarations diff

+ Adj
+ DiHypergraph
+ EAdj
+ EAdj.exists_vertex
+ EAdj.inter_nonempty
+ IsBFHypergraph
+ IsBHypergraph
+ IsEmpty
+ IsEmpty.eq
+ IsEmpty.not_isNonempty
+ IsEmpty.not_mem_edge
+ IsEmpty.not_mem_vertex
+ IsFHypergraph
+ IsIsolated
+ IsNonEndless
+ IsNonempty
+ IsNonempty.not_isEmpty
+ coe_nonempty
+ dst_isSubset_vertexSet
+ edge_not_mem_empty
+ edge_src_dst_isSubset_vertexSet
+ emptyDiHypergraph
+ forall_of_forall_verts_dst
+ forall_of_forall_verts_src
+ head_star
+ isBFHypergraph_emptyDiHypergraph
+ isBHypergraph_emptyDiHypergraph
+ isEmpty_empty_hypergraph
+ isEmpty_eq_empty_hypergraph
+ isEmpty_iff_forall_not_mem
+ isEmpty_or_isNonempty
+ isFHypergraph_emptyDiHypergraph
+ isIsolated_headStar_empty
+ isIsolated_headStar_isEmpty
+ isIsolated_negativeDegree_zero
+ isIsolated_negativeStar_empty
+ isIsolated_negativeStar_isEmpty
+ isIsolated_positiveDegree_zero
+ isIsolated_positiveStar_empty
+ isIsolated_positiveStar_isEmpty
+ isIsolated_tailStar_empty
+ isIsolated_tailStar_isEmpty
+ isNonEndless_emptyDiHypergraph
+ mem_vertexSet_of_mem_edgeSet_dst
+ mem_vertexSet_of_mem_edgeSet_src
+ mem_vertexSet_of_mem_edgeSet_src_dst
+ negative_degree
+ negative_star
+ not_isEmpty
+ not_isNonempty
+ positive_degree
+ positive_star
+ src_isSubset_vertexSet
+ tail_star

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

[mathlib4-merge-conflict-bot]

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