Commit 2025-03-20 16:39 07d2b9ef

chore(Data/Set): split long file Function.lean (#23149) This PR splits the long file Data.Set.Function into a few chunks:

• Data.Set.Function now focusses on lemmas for predicates such as EqOn, InjOn, MapsTo, ...
• Data.Set.Piecewise is a new file for results on the definiton Set.piecewise.
• Data.Set.Prod received some upstreamed results on graphOn and the vertical line test.
• Data.Set.Restrict is a new file for the definition of Set.restrict and some basic results.