Zulip Chat Archive

Stream: maths

Topic: integral of positive measurable functions


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 14:35):

src#measure_theory.lintegral

view this post on Zulip Rob Lewis (Jul 18 2020 at 14:35):

Thanks!

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 14:35):

(link doesn't work)

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 14:35):

Wait a minute

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 14:36):

Fixed the link


Last updated: May 10 2021 at 08:14 UTC