Fill finite unions in the null-set boolean algebra - #711

Open

Chessing234 wants to merge 1 commit into

teorth:mainfrom

Chessing234:feat/null-union-mem

Chessing234 commented Sep 7, 2026 •

edited

Loading

Contributor

Summary

The union of two null sets is null by finite subadditivity of outer measure. If either complement is null, the complement of the union is a subset of a null set.

Test plan

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


          Fill finite unions in the null-set boolean algebra.

09c16f4

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

Labels

None yet