mathlib

e1560a31 - feat(measure_theory/borel_space): continuity set of a function is measurable (#4967)

feat(measure_theory/borel_space): continuity set of a function is measurable (#4967) * Move the definition of `is_Gδ` and basic lemmas to a separate file. * Prove that `{x | continuous_at f x}` is a Gδ set provided that the codomain is a uniform space with countable basis of the uniformity filter (e.g., an `emetric_space`). In particular, this set is measurable. * Rename `nhds_le_uniformity` to `supr_nhds_le_uniformity`. * Add new `nhds_le_uniformity` without `⨆` in the statement. * Add `uniform.continuous_at_iff_prod`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>