Commit 2026-05-26 14:39 ea088ce5

View on Github →

feat: a lemma about the symmetric difference of unions (#38536) Created with the help of Codex.

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.iUnion_symmDiff_iUnion_subset

added theorem Set.iUnion_symmDiff_subset

added theorem Set.sUnion_symmDiff_sUnion_subset

added theorem Set.sUnion_symmDiff_subset

added theorem Set.symmDiff_iUnion_subset

added theorem Set.symmDiff_sUnion_subset

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iSup_symmDiff_le

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.sSup_symmDiff_le

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.sSup_symmDiff_sSup_le

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.symmDiff_iSup_le

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.symmDiff_sSup_le