Commit 2022-07-13 02:40 2a325960

View on Github →

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.

Estimated changes

Modified src/data/finsupp/basic.lean

added theorem finsupp.apply_eq_of_mem_graph

added def finsupp.graph

added theorem finsupp.graph_eq_empty

added theorem finsupp.graph_inj

added theorem finsupp.graph_injective

added theorem finsupp.graph_zero

added theorem finsupp.image_fst_graph

added theorem finsupp.mem_graph_iff

added theorem finsupp.mk_mem_graph

added theorem finsupp.mk_mem_graph_iff

added theorem finsupp.not_mem_graph_snd_zero