Fill that Lebesgue measure is countably additive - #714

Open

Chessing234 wants to merge 1 commit into

teorth:mainfrom

Chessing234:feat/lebesgue-countably-additive

Chessing234 commented Sep 7, 2026 •

edited

Loading

Contributor

Summary

Lebesgue measure as a finitely additive measure is countably additive: the algebra is a sigma-algebra and disjoint countable unions are handled by the existing outer-measure identity.

Test plan

lake build Analysis.MeasureTheory.Section_1_4_3; CI covers the module.


          Fill that Lebesgue measure is countably additive.

c00730c

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet