refactor(topology/uniform_space/basic): review API (#18516)
### API about uniform embeddings
* Add `mk_iff` to `uniform_inducing` and `uniform_embedding`.
* Move lemmas about `uniform_inducing` up.
* Add `uniform_inducing.comap_uniform_space`, `uniform_inducing_iff'`, and `filter.has_basis.uniform_inducing_iff`.
* Add `uniform_embedding_iff'`, `filter.has_basis.uniform_embedding_iff'`, and `filter.has_basis.uniform_embedding_iff`.
* Drop `uniform_embedding_def` and `uniform_embedding_def'`.
* Add `uniform_embedding_iff_uniform_inducing`.
### Other changes
* Add `rescale_to_shell_semi_normed_zpow` and `rescale_to_shell_zpow`.
* Generalize `continuous_linear_map.antilipschitz_of_uniform_embedding` to `continuous_linear_map.antilipschitz_of_embedding`, add an even more general version `linear_map.antilipschitz_of_comap_nhds_le`.
* Use `fully_applied := ff` to generate `equiv.prod_congr_apply`.
* Use `edist := λ _ _, 0` in `metric_space` instances for `empty` and `punit`.
* Add `inducing.injective`, `inducing.embedding`, and `embedding_iff_inducing`
* Allow `Sort*`s in `filter.has_basis.uniform_continuous_iff` and `filter.has_basis.uniform_continuous_on_iff`.
* Rename
* `metric.of_t0_pseudo_metric_space` to `metric_space.of_t0_pseudo_metric_space`;
* `emetric.of_t0_pseudo_emetric_space` to `emetric_space.of_t0_pseudo_emetric_space`;
* `metric.metric_space.to_emetric_space` to `metric_space.to_emetric_space`;
* `uniform_embedding_iff'` to `emetric.uniform_embedding_iff'`
