Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-07 07:05 fabad7ec

View on Github →

feat(order/symm_diff): More symmetric difference lemmas (#13133) A few more symm_diff lemmas.

Estimated changes

added theorem eq_of_sdiff_eq_sdiff
added theorem inf_sdiff_distrib_left
added theorem inf_sdiff_right_comm
added theorem sdiff_eq_comm
added theorem sdiff_eq_symm
added theorem sdiff_sdiff_le
added theorem sdiff_sup_sdiff_cancel
deleted theorem sdiff_symm
added theorem inf_inf_distrib_left
added theorem inf_inf_distrib_right
added theorem sup_sup_distrib_left
added theorem sup_sup_distrib_right
added theorem sup_sdiff_symm_diff