Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-08 05:41 f585481b

View on Github →

feat(data/set/prod): add lemmas about set.pi (#16828)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.disjoint_iff_inter_eq_empty

Modified src/data/set/lattice.lean

deleted theorem set.disjoint_iff_inter_eq_empty

Modified src/data/set/prod.lean

added theorem set.disjoint_univ_pi

added theorem set.pi_subset_pi_iff

modified theorem set.univ_pi_eq_empty_iff

added theorem set.univ_pi_subset_univ_pi_iff