mathlib

2a325960 - feat(data/finsupp/basic): graph of a finitely supported function (#15197)

feat(data/finsupp/basic): graph of a finitely supported function (#15197) We define the graph of a finitely supported function, i.e. the finset of input/output pairs, and prove basic results. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>