feat(Combinatorics): incidence-based HypergraphLike class

[Jun2M]

This PR introduces an alternative definition of HyperGraphLike based on incidence.
This is alternative to #36743.
See discussion at (#graph theory > HasAdj) for more information.

---

[github-actions]

PR summary 1e926ccaba

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.GraphLike.Basic (new file)	880
Mathlib.Combinatorics.GraphLike.Walks.Dart (new file)	881
3 files Mathlib.Combinatorics.Digraph.GraphLike (new file) Mathlib.Combinatorics.Graph.GraphLike (new file) Mathlib.Combinatorics.GraphLike.Walks.Basic (new file)	882
Mathlib.Combinatorics.SimpleGraph.GraphLike (new file)	883

---

Declarations diff

+ Adj
+ Adj'
+ Adj.left_mem
+ Adj.right_mem
+ Adj.symm
+ Dart
+ Directed
+ GraphLike
+ HyperGraphLike
+ IncidenceType
+ IncidenceType.dir_of_ne
+ IncidenceType.edge
+ IncidenceType.fwd_or_bwd_of_eq
+ IncidenceType.source
+ IncidenceType.target
+ IsIncident.edge_mem
+ IsIncident.inc_inj
+ IsIncident.inc_mem
+ IsIncident.inj
+ IsIncident.isSource
+ IsIncident.isSource_or_isTarget
+ IsIncident.isTarget
+ IsIncident.mem_edgeFun
+ IsIncident.mem_endPoint
+ IsIncident.unique_or_bot
+ IsIncident.vert_mem
+ IsLink
+ IsLink.adj
+ IsLink.edge_inj_of_isLink_of_directed
+ IsLink.edge_inj_of_isLink_of_undirected
+ IsLink.edge_mem
+ IsLink.eq_or_eq_of_isLink
+ IsLink.incMatrixWith_col_eq_of_directed
+ IsLink.incMatrixWith_col_eq_of_undirected
+ IsLink.incMatrix_col_eq
+ IsLink.left_mem
+ IsLink.right_mem
+ IsSource.exists_isIncident
+ IsSource.mem
+ IsSource.not_isTarget
+ IsTarget.exists_isIncident
+ IsTarget.mem
+ IsTarget.not_isSource
+ Loopless
+ Nil
+ Nil.eq
+ Nil.eq_nil
+ NoMultiEdge
+ Undirected
+ Walk
+ _root_.HyperGraphLike.DartAdj
+ _root_.HyperGraphLike.adj_iff_exists_dart
+ _root_.HyperGraphLike.isLink_iff_exists_dart
+ adj_comm
+ adj_of_length_eq_one
+ coe_edges_toFinset
+ coe_support
+ cons'
+ cons_map_target_darts
+ cons_tail_support
+ dart_source_mem_support_of_mem_darts
+ darts
+ darts_cons
+ darts_eq_nil
+ darts_injective
+ darts_nil
+ darts_nodup_of_support_nodup
+ darts_ofDarts
+ degree
+ disjoint_preimage_of_disjoint
+ dom_edgeFun
+ dom_endPoint
+ edge
+ edgeFun
+ edgeFun_eq
+ edgeFun_preimage_singleton_eq_dir_of_isLink_nonloop
+ edgeFun_preimage_singleton_eq_fwd_bwd_of_isLink_loop
+ edgeFun_preimage_singleton_injOn
+ edgeFun_preimage_singleton_injOn_of_GraphLike
+ edgeSet
+ edgeSet_cons
+ edgeSet_nil
+ edge_eq_iff_of_directed
+ edge_eq_iff_of_undirected
+ edge_eq_iff_source
+ edge_eq_iff_target
+ edge_eq_of_isIncident_fst
+ edge_eq_of_isIncident_snd
+ edge_mem
+ edge_mem_edgeFun_fst
+ edge_mem_edgeFun_iff_fst_or_snd
+ edge_mem_edgeFun_snd
+ edges
+ edges_cons
+ edges_eq_nil
+ edges_nil
+ edges_ofDarts
+ edges_subset_edgeSet
+ endPoint
+ endPoint_eq
+ end_mem_support
+ end_mem_tail_support
+ end_mem_tail_support_of_ne
+ eq_of_length_eq_zero
+ eq_of_source_target_eq_of_directed
+ eq_of_source_target_eq_of_undirected
+ exists_boundary_dart
+ exists_eq_cons_of_ne
+ exists_isLink_of_mem_edgeSet
+ exists_isSource_of_mem_edgeSet
+ exists_isTarget_of_mem_edgeSet
+ exists_length_eq_one_iff
+ exists_length_eq_zero_iff
+ exists_pair_mem_edgeFun_iff
+ ext
+ fst
+ fst_isSource
+ fst_mem
+ fst_ne_snd
+ fst_or_snd_of_isIncident
+ getLast_support
+ head_support
+ inc1
+ inc1_edge
+ inc1_ne_inc2
+ inc1_source
+ inc1_target
+ inc2
+ inc2_edge
+ inc2_source
+ inc2_target
+ incMatrix
+ incMatrixWith
+ incMatrixWith_apply_of_directed
+ incMatrixWith_apply_of_undirected
+ incMatrix_col_eq
+ incMatrix_same_apply
+ incs_ext
+ instDecidable
+ instDecidableEq
+ instInhabited
+ instance (p : Walk G v w) : Decidable p.Nil
+ instance : Directed V (Bool × V × V) (V × V) (Digraph V)
+ instance : GraphLike V (Bool × V × V) (V × V) (Digraph V)
+ instance : GraphLike V (IncidenceType V E) E (Graph V E)
+ instance : GraphLike V (V × V) (Sym2 V) (SimpleGraph V)
+ instance : HyperGraphLike V (Bool × V × V) (V × V) (Digraph V)
+ instance : HyperGraphLike V (IncidenceType V E) E (Graph V E)
+ instance : HyperGraphLike V (V × V) (Sym2 V) (SimpleGraph V)
+ instance : Loopless V (V × V) (Sym2 V) (SimpleGraph V)
+ instance : NoMultiEdge V (Bool × V × V) (V × V) (Digraph V)
+ instance : NoMultiEdge V (V × V) (Sym2 V) (SimpleGraph V)
+ instance : Std.Symm (Adj G)
+ instance : Undirected V (IncidenceType V E) E (Graph V E)
+ instance : Undirected V (V × V) (Sym2 V) (SimpleGraph V)
+ instance [DecidableEq I] : DecidableEq (Dart G)
+ isChain_adj_cons_support
+ isChain_adj_support
+ isChain_dartAdj_cons_darts
+ isChain_dartAdj_darts
+ isIncident_edgeFun_endPoint
+ isLink_iff_exists_incidenceType
+ isLink_iff_of_undirected
+ isSource_iff
+ isSource_of_mem_incs
+ isTarget_of_mem_incs
+ length
+ length_cons
+ length_darts
+ length_edges
+ length_eq_zero_iff
+ length_nil
+ length_ofDarts
+ length_ofSupport
+ length_support
+ map_source_darts
+ map_source_darts_append
+ map_target_darts
+ mem_darts_iff_fst_snd_infix_support
+ mem_darts_iff_infix_support
+ mem_edgeFun_iff_exists_isIncident
+ mem_edgeFun_inc1_iff
+ mem_edgeFun_inc2_iff
+ mem_edgeFun_mem_endPoint_iff_isIncident
+ mem_edgeSet
+ mem_endPoint_iff_exists_isIncident
+ mem_incs_of_mem_edgeFun
+ mem_incs_of_mem_endPoint
+ mem_support_iff
+ mem_support_nil_iff
+ nil'
+ nil_iff_eq_nil
+ nil_iff_length_eq
+ nil_iff_support_eq
+ nil_iff_support_eq'
+ nil_nil
+ no_loops
+ no_loops'
+ notNilRec
+ notNilRec_cons
+ not_nil_cons
+ not_nil_iff
+ not_nil_iff_lt_length
+ not_nil_of_ne
+ ofDarts
+ ofDarts_cons_cons
+ ofDarts_singleton
+ ofSupport
+ ofSupport_cons_cons
+ ofSupport_singleton
+ order
+ order_eq_two
+ order_eq_two_of_isLink
+ preimage_empty
+ snd
+ snd_isTarget
+ snd_mem
+ source
+ source_darts_getElem
+ source_eq_iff
+ source_eq_of_isIncident_fst
+ source_isIncident
+ source_mem
+ source_target_inj_of_directed
+ source_target_inj_of_undirected
+ start_mem_support
+ support
+ support_cons
+ support_getElem_length
+ support_getElem_zero
+ support_ne_nil
+ support_nil
+ support_nonempty
+ support_ofSupport
+ support_subset_support_cons
+ sym2
+ sym2_eq_iff
+ sym2_eq_mk_iff
+ sym2_symm
+ symm
+ symm_edge
+ symm_fst
+ symm_involutive
+ symm_snd
+ symm_source
+ symm_symm
+ symm_target
+ target
+ target_darts_getElem
+ target_eq_iff
+ target_eq_of_isIncident_snd
+ target_isIncident
+ target_mem
+ toProd
+ toProd_eq_mk_iff
+ unique_isIncident_of_mem_incs
+ val_eq_iff

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 1e926ccaba
Reference commit c6da5183b5

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!