[Merged by Bors] - feat(MeasureTheory/MeasurableSpace/Basic): add map_comap_eq_of_surjective and measurable_comap_iff_right#41090

teorth wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

teorth:comapteorth/mathlib4:comapCopy head branch name to clipboard