Commit 2023-12-27 10:11 13465267

View on Github →

feat: When a \ b = b \ a (#9109) and other simple order lemmas From LeanAPAP and LeanCamCombi

Estimated changes

added theorem himp_eq_left
added theorem himp_le_iff
added theorem himp_ne_right
added theorem sdiff_eq_right
added theorem sdiff_ne_right
modified theorem ciInf_le'
added theorem ciInf_le_of_le'
modified theorem csInf_le'
modified theorem Finset.inf'_eq_csInf_image
modified theorem Finset.inf'_id_eq_csInf
modified theorem Finset.sup'_eq_csSup_image
modified theorem Finset.sup'_id_eq_csSup
added theorem Codisjoint.eq_iff
added theorem Codisjoint.ne_iff
added theorem Disjoint.eq_iff
added theorem Disjoint.ne_iff
added theorem himp_eq_himp_iff
added theorem himp_ne_himp_iff
added theorem sdiff_eq_sdiff_iff
added theorem sdiff_ne_sdiff_iff