Theorem set.eq_univ_of_forall

feat(data/analysis): calculations with filters / topologies + misc

refactor(algebra/lattice): use *experiment files, move set.lattice to .basic

refactor(*): import content from lean/library/data and library_dev