Commit 2020-11-11 13:39 e1560a31

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.