Zulip Chat Archive
Stream: maths
Topic: integral of positive measurable functions
Rob Lewis (Jul 18 2020 at 14:34):
The website build is breaking after the measure theory refactor because measure_theory.measure.integral was renamed. This was the entry integral of positive measurable functions in the overview. What's the new declaration corresponding to this topic?
Yury G. Kudryashov (Jul 18 2020 at 14:35):
Rob Lewis (Jul 18 2020 at 14:35):
Thanks!
Yury G. Kudryashov (Jul 18 2020 at 14:35):
(link doesn't work)
Yury G. Kudryashov (Jul 18 2020 at 14:35):
Wait a minute
Yury G. Kudryashov (Jul 18 2020 at 14:36):
Fixed the link
Last updated: May 02 2025 at 03:31 UTC