Theorem set.image_subset_iff'

feat(analysis/topology/completion): comm_ring on separation quotient, completion (separation_quotient A) is equivalent to completion A

feat(analysis/topology/topological_structure): ideal closure is ideal