Commit 2021-10-22 15:58 d23b8334

View on Github →

chore(data/set/lattice): add @[simp] to a few lemmas (#9883) Add @[simp] to Union_subset_iff, subset_Inter_iff, sUnion_subset_iff, and subset_sInter_iff (new lemma).

Estimated changes

Modified src/data/set/lattice.lean

modified theorem set.Union_subset_iff

modified theorem set.sUnion_subset_iff

modified theorem set.subset_Inter_iff

added theorem set.subset_sInter_iff