Commit 2024-10-08 16:10 92fd0f87

View on Github →

feat: graphOn API (#17303) From PFR

Estimated changes

Modified Mathlib/Data/Set/Function.lean

added theorem Set.fst_injOn_graph

added theorem Set.graphOn_comp

added theorem Set.graphOn_eq_empty

added theorem Set.graphOn_inj

added theorem Set.graphOn_nonempty

added theorem Set.graphOn_univ_eq_range

added theorem Set.graphOn_univ_inj

added theorem Set.graphOn_univ_injective

added theorem Set.image_snd_graphOn

added theorem Set.mem_graphOn