feat(equiv|set|topology): various additions (#5656)
define sigma_compact_space
update module doc for topology/subset_properties
define shearing
some lemmas in set.basic, equiv.mul_add and topology.instances.ennreal
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
