feat(*): random lemmas about sets and filters (#3118)
This is the first in a series of PR that will culminate in a proof of Heine's theorem (a continuous function from a compact separated uniform space to any uniform space is uniformly continuous). I'm slicing a 600 lines files into PRs. This first PR is only about sets, filters and a bit of topology. Uniform spaces stuff will come later.
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
