Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-07 13:02 46d10092

View on Github →

feat(analysis/metric_space): Isometries (#657)

Estimated changes

Created src/topology/metric_space/isometry.lean

added theorem emetric.isometry.diam_image

added theorem isometric.coe_eq_to_equiv

added theorem isometric.coe_eq_to_homeomorph

added theorem isometric.image_symm

added theorem isometric.preimage_symm

added theorem isometric.range_coe

added theorem isometric.self_comp_symm

added theorem isometric.symm_comp_self

added theorem isometric.to_homeomorph_to_equiv

added structure isometric

added theorem isometry.comp

added theorem isometry.continuous

added theorem isometry.dist_eq

added theorem isometry.edist_eq

added theorem isometry.injective

added theorem isometry.inv

added theorem isometry.isometric_on_range

added theorem isometry.isometric_on_range_apply

added theorem isometry.uniform_embedding

added def isometry

added theorem isometry_emetric_iff_metric

added theorem isometry_id

added theorem isometry_subsingleton

added theorem isometry_subtype_val

added theorem metric.isometry.diam_image