Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-29 06:34 8a697e5d

View on Github →

feat(data/set/basic): symm_diff lemmas (#17051) A few lemma about symm_diff, and their translation to set.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.image_symm_diff

added theorem set.subset_image_symm_diff

added theorem set.subset_symm_diff_union_symm_diff_left

added theorem set.subset_symm_diff_union_symm_diff_right

added theorem set.symm_diff_eq_empty

added theorem set.symm_diff_nonempty

Modified src/order/symm_diff.lean

added theorem codisjoint.bihimp_inf_bihimp_le_left

added theorem codisjoint.bihimp_inf_bihimp_le_right

added theorem disjoint.le_symm_diff_sup_symm_diff_left

added theorem disjoint.le_symm_diff_sup_symm_diff_right