add big_sepS_insert_2' and big_sepS_union_2
-
big_sepS_insert_2'
is likebig_sepS_insert_2
but "inserts" into the set from the right rather than the left. -
big_sepS_union_2
is the direction ofbig_sepS_union
that holds without disjointness (for affine assertions). I was quite surprised not to already find this, did I miss something?