Commit 2021-01-10 14:47 b0c35d12

chore(order/filter/basic): a few simp lemmas (#5685)

Changes in order/filter/basic

• add filter.inter_mem_sets_iff;
• rename filter.Inter_mem_sets to filter.bInter_mem_sets, make it an iff [simp] lemma;
• add a version filter.bInter_finset_mem_sets with a protected alias finset.Inter_mem_sets;
• rename filter.sInter_mem_sets_of_finite to filter.sInter_mem_sets, make it an iff [simp] lemma;
• rename filter.Inter_mem_sets_of_fintype to filter.Inter_mem_sets, make it an iff [simp] lemma
• add eventually versions of the *Inter_mem_sets lemmas.

New @[mono] attributes

• set.union_subset_union and set.inter_subset_inter instead of monotone_union and monotone_inter; mono* failed to make a progress with s ∩ t ⊆ s' ∩ t' goal.
• set.image2_subset
• closure_mono