Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-07 15:40 1eb3ae42

View on Github →

feat(order/symm_diff): symmetric difference operator (#6469)

Estimated changes

Modified src/order/boolean_algebra.lean

added theorem compl_eq_iff_is_compl

added theorem disjoint.disjoint_sdiff_left

added theorem disjoint.disjoint_sdiff_right

deleted theorem disjoint_sdiff

added theorem disjoint_sdiff_self_left

added theorem disjoint_sdiff_self_right

added theorem eq_compl_iff_is_compl

added theorem sdiff_sdiff_self

Modified src/order/bounded_lattice.lean

added theorem disjoint.eq_bot_of_le

added theorem disjoint.of_disjoint_inf_of_le'

added theorem disjoint.of_disjoint_inf_of_le

Created src/order/symm_diff.lean

added theorem bot_symm_diff

added theorem compl_symm_diff

added theorem compl_symm_diff_self

added theorem disjoint.disjoint_symm_diff_of_disjoint

added theorem disjoint.symm_diff_eq_sup

added theorem disjoint_symm_diff_inf

added theorem is_compl.symm_diff_eq_top

added theorem sdiff_symm_diff'

added theorem sdiff_symm_diff

added theorem sdiff_symm_diff_self

added def symm_diff

added theorem symm_diff_assoc

added theorem symm_diff_bot

added theorem symm_diff_comm

added theorem symm_diff_compl_self

added theorem symm_diff_def

added theorem symm_diff_eq

added theorem symm_diff_eq_bot

added theorem symm_diff_eq_iff_sdiff_eq

added theorem symm_diff_eq_left

added theorem symm_diff_eq_right

added theorem symm_diff_eq_sup

added theorem symm_diff_eq_sup_sdiff_inf

added theorem symm_diff_eq_top_iff

added theorem symm_diff_eq_xor

added theorem symm_diff_le_sup

added theorem symm_diff_left_inj

added theorem symm_diff_right_inj

added theorem symm_diff_sdiff

added theorem symm_diff_sdiff_left

added theorem symm_diff_sdiff_right

added theorem symm_diff_self

added theorem symm_diff_symm_diff_left

added theorem symm_diff_symm_diff_right'

added theorem symm_diff_symm_diff_right

added theorem symm_diff_symm_diff_self'

added theorem symm_diff_symm_diff_self

added theorem symm_diff_top

added theorem top_symm_diff