Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-17 18:12 57bbd9ec

View on Github →

chore(order/symm_diff): Generalize to co-Heyting algebras (#16282) Generalize the symm_diff material from (generalized_)boolean_algebra to (generalized_)coheyting_algebra.

Estimated changes

added theorem finset.coe_symm_diff
added theorem finset.mem_symm_diff
added theorem set.le_iff_subset
added theorem set.lt_iff_ssubset
added theorem set.mem_symm_diff
modified theorem compl_symm_diff_self
added theorem hnot_symm_diff_self
added theorem inf_sup_symm_diff
modified theorem is_compl.symm_diff_eq_top
added theorem sdiff_symm_diff_eq_sup
modified def symm_diff
modified theorem symm_diff_compl_self
modified theorem symm_diff_def
modified theorem symm_diff_eq_iff_sdiff_eq
modified theorem symm_diff_eq_sup_sdiff_inf
added theorem symm_diff_hnot_self
added theorem symm_diff_le
added theorem symm_diff_le_iff
modified theorem symm_diff_le_sup
added theorem symm_diff_of_ge
added theorem symm_diff_of_le
modified theorem symm_diff_sdiff
added theorem symm_diff_sdiff_eq_sup
added theorem symm_diff_sdiff_inf
added theorem symm_diff_sup_inf
added theorem symm_diff_top'
modified theorem symm_diff_top
added theorem top_symm_diff'
modified theorem top_symm_diff