@somethingsome If you want to turn arbitrary maths into code, you should take a look at interactive proof assistants. I'm a fan of https://leanprover-community.

@somethingsome If you want to turn arbitrary maths into code, you should take a look at interactive proof assistants. I'm a fan of https://leanprover-community.github.io/ https://leanprover-community.github.io/ It has Borel spaces: https://leanprover-community.github.io/mathlib_docs/measure_theory/borel_space.html https://leanprover-community.github.io/mathlib_docs/measure_...