Fill null, atomic, restriction, and infimum constructors for boolean algebras

[Chessing234]

Summary

• Null algebra: empty is null, complement swaps the two disjuncts, and null sets (and their complements) are Lebesgue measurable.
• Atomic algebra: empty is the empty union of atoms; the discrete partition is singletons; the trivial partition is a single copy of univ.
• Restriction along a subset is preimage, so empty/complement/union are those of the ambient algebra.
• Infima of algebras are pointwise.

Test plan

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