Skip to content

Fill empty and complement for the elementary boolean algebra - #689

Open
Chessing234 wants to merge 1 commit into
teorth:mainfrom
Chessing234:feat/elementary-boolean-algebra
Open

Fill empty and complement for the elementary boolean algebra#689
Chessing234 wants to merge 1 commit into
teorth:mainfrom
Chessing234:feat/elementary-boolean-algebra

Conversation

@Chessing234

Copy link
Copy Markdown
Contributor

Summary

  • IsElementary.empty gives measurability of ∅.
  • Complement is Or.symm on IsElementary E ∨ IsElementary Eᶜ.
  • Finite union left sorry (mixed elementary / co-elementary cases).

Test plan

  • lake build Analysis.MeasureTheory.Section_1_4_1

Made with Cursor

The empty box is elementary; complement swaps the two disjuncts.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant