mathlib

38977584 - feat(measure_theory): prove that more functions are measurable (#4266)

feat(measure_theory): prove that more functions are measurable (#4266) Mostly additions to `borel_space`. Generalize `measurable_bsupr` and `measurable_binfi` to countable sets (instead of encodable underlying types). Use the lemma `countable_encodable` to get the original behavior. Some cleanup in `borel_space`: more instances are in `variables`, and lemmas with the same instances a bit more. One downside: there is a big import bump in `borel_space`, it currently imports `hahn_banach`. This is (only) used in `measurable_smul_const`. If someone has a proof sketch (in math) of `measurable_smul_const` that doesn't involve Hahn Banach (and that maybe generalizes `real` to a topological field or something), please let me know.