Theorem quot_mk_image_univ_eq

feat(data/multiset): working on multisets, fix rcases bug

chore(topology): move general theorems to the corresponding theories

construct reals as complete, linear ordered field