mathlib3

964fbc2e - feat(data/set): gluing functions

feat(data/set): gluing functions - glue together functions from families of functions and prove some things about the function resulting from the gluing.