Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-08 20:36 84a1bd6a

View on Github →

refactor(topology/metric_space/basic): add pseudo_metric_space.to_bornology' (#13927)

  • add pseudo_metric_space.to_bornology' and pseudo_metric_space.replace_bornology;
  • add metric.is_bounded_iff and a few similar lemmas;
  • fix instances for subtype, prod, pi, and pi_Lp to use the correct bornology`;
  • add lipschitz_with.to_locally_bounded_map and lipschitz_with.comap_cobounded_le;
  • add antilipschitz_with.tendsto_cobounded.

Estimated changes

modified def enorm.emetric_space
added theorem pi_Lp.aux_cobounded_eq
added theorem metric.is_bounded_iff