Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-25 21:56 e04892ec

View on Github →

feat(topology/metric_space/isometry): add_left/right, neg (#2234) Also add some lemmas from equiv namespace to isometric.

Estimated changes

Modified src/topology/metric_space/isometry.lean

added theorem isometric.apply_symm_apply

added theorem isometric.eq_symm_apply

added theorem isometric.ext

added theorem isometric.symm_apply_apply

added theorem isometric.symm_apply_eq

added theorem isometric.trans_apply