[Merged by Bors] - feat: if Y = f(X) then Y is X-measurable#39728

mathlib-splicebot[bot] wants to merge 2 commits into

masterleanprover-community/mathlib4:masterfrom

splice-bot/pr-37259-Mathlib-MeasureTheory-MeasurableSpace-Basic.lean-25cdbec65a-a6bvmbsleanprover-community/mathlib4_copy:splice-bot/pr-37259-Mathlib-MeasureTheory-MeasurableSpace-Basic.lean-25cdbec65a-a6bvmbsCopy head branch name to clipboard