Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-26 13:12 187bfa52

View on Github →

feat(set/basic): additions to prod (#3943) Also add one lemma about Inter.

Estimated changes

Modified src/data/set/basic.lean

modified theorem set.insert_prod

added theorem set.mk_preimage_prod_left_eq_empty

added theorem set.mk_preimage_prod_left_eq_if

added theorem set.mk_preimage_prod_right_eq_empty

added theorem set.mk_preimage_prod_right_eq_if

modified theorem set.prod_eq_empty_iff

modified theorem set.prod_insert

added theorem set.prod_univ

added theorem set.univ_prod

Modified src/data/set/lattice.lean

added theorem set.Inter_set_of