Commit 2026-09-15 17:41 1323ec21
View on Github →chore(Order/CompleteBooleanAlgebra): dualize symmDiff theorems (#39905)
Dualize some symmDiff theorems, and also generalize them from CompleteBooleanAlgebra to Order.Coframe.
Estimated changes
deleted theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.biSup_symmDiff_biSup_le
deleted theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iSup_symmDiff_iSup_le
deleted theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iSup_symmDiff_le
added theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.le_biInf_bihimp_biInf
added theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.le_bihimp_iInf
added theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.le_bihimp_sInf
added theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.le_iInf_bihimp
added theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.le_iInf_bihimp_iInf
added theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.le_sInf_bihimp
added theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.le_sInf_bihimp_sInf
deleted theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.sSup_symmDiff_le
deleted theorem Order.Frame.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.sSup_symmDiff_sSup_le