feat(topology): add some lemmas (#9907)
* From the sphere eversion project
* Add compositional version `continuous.fst` of `continuous_fst`, compare `measurable.fst`.
* Add `comp_continuous_at_iff` and `comp_continuous_at_iff'` for `homeomorph` (and for `inducing`).
* Add some variants of these (requested by review).
