Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-19 08:03 b1cb48d1

View on Github →

feat(data/set): simple lemmas, renaming (#1137)

  • feat(data/set): simple lemmas, renaming
  • improve projection lemmas
  • arguments order

Estimated changes

added theorem set.fst_image_prod
modified theorem set.preimage_id
added theorem set.snd_image_prod
added theorem set.Inter_inter
added theorem set.Union_diff
added theorem set.Union_inter
added theorem set.Union_union
added theorem set.bUnion_inter
added theorem set.diff_Inter
deleted theorem set.diff_Inter_left
added theorem set.diff_Union
deleted theorem set.diff_Union_left
deleted theorem set.diff_Union_right
added theorem set.inter_Inter
deleted theorem set.inter_Inter_left
deleted theorem set.inter_Inter_right
added theorem set.inter_Union
deleted theorem set.inter_Union_left
deleted theorem set.inter_Union_right
added theorem set.inter_bUnion
added theorem set.union_Inter
deleted theorem set.union_Inter_left
added theorem set.union_Union
deleted theorem set.union_Union_left
deleted theorem set.union_Union_right