mathlib

b3aa0524 - feat(combinatorics/simple_graph/basic): introduce incidence sets, graph construction from relation (#5191)

feat(combinatorics/simple_graph/basic): introduce incidence sets, graph construction from relation (#5191) Add incidence sets and some lemmas, including a proof of equivalence between the neighbor set of a vertex and its incidence set. Add a graph construction from a given relation. Definitions and lemmas adapted from [simple_graphs2](https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph/basic.lean#L317) Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>