mathlib

5f70cd95 - chore(measure_theory/function/ae_eq_fun): replace topological assumptions by measurability assumptions (#11981)

chore(measure_theory/function/ae_eq_fun): replace topological assumptions by measurability assumptions (#11981) Since the introduction of the `has_measurable_*` typeclasses, the topological assumptions in that file are only used to derive the measurability assumptions. This PR removes that step. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>