Skip to content

add big_sepS_insert_2' and big_sepS_union_2

Ralf Jung requested to merge ralf/big_sepS into master
  • big_sepS_insert_2' is like big_sepS_insert_2 but "inserts" into the set from the right rather than the left.
  • big_sepS_union_2 is the direction of big_sepS_union that holds without disjointness (for affine assertions). I was quite surprised not to already find this, did I miss something?

Merge request reports