Commit 2021-04-02 21:56 278ad338

View on Github →

refactor(topology/metric_space/isometry): generalize to pseudo_metric (#6910) This is part of a series of PR to have the theory of semi_normed_group (and related concepts) in mathlib. We generalize here isometry to pseudo_emetric_space and pseudo_metric_space.

Estimated changes

Modified src/analysis/normed_space/dual.lean

Modified src/topology/metric_space/isometry.lean

modified theorem algebra_map_isometry

modified def isometric.mk'

modified structure isometric

modified theorem isometry.closed_embedding

modified theorem isometry.comp_continuous_iff

modified theorem isometry.comp_continuous_on_iff

modified theorem isometry.diam_image

modified theorem isometry.diam_range

modified theorem isometry.dist_eq

modified theorem isometry.edist_eq

modified theorem isometry.injective

modified def isometry.isometric_on_range

modified theorem isometry.isometric_on_range_apply

modified theorem isometry.uniform_embedding

modified def isometry

modified theorem isometry_emetric_iff_metric