Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-13 23:50 9dfe6490

View on Github →

feat(data/{set,finset}/prod): lemmas about disjoint and intersections (#17496)

Estimated changes

Modified src/data/finset/prod.lean

added theorem finset.disj_union_product

added theorem finset.disjoint_product

added theorem finset.inter_product

added theorem finset.product_disj_union

added theorem finset.product_inter

added theorem finset.product_inter_product

Modified src/data/set/prod.lean

added theorem set.disjoint_prod

added theorem set.inter_prod

added theorem set.prod_inter