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):

src#measure_theory.lintegral

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: Dec 20 2023 at 11:08 UTC