feat(topology): is_closed_proj_of_compact (#2069)
* feat(lattice): add inf_le_inf_left/right
* feat(set/lattice): image_inter_subset
* feat(set/lattice): push_pull
* feat(order/filter): push_pull and product notation
* feat(topology/subset_properties): is_closed_proj_of_compact
* feat(set/lattice): push_pull'
* fix(order/filter): forgotten doc
* lint (including old missing docstrings in filter).
* Apply Yury's suggestions.
* Forgotten style fix
* urkud's suggestions
Co-Authored-By: Yury G. Kudryashov <urkud@urkud.name>
* Update src/order/filter/basic.lean
Co-Authored-By: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
