Commit 2023-03-01 18:06 195fcd60

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'