Commit 2023-03-08 06:41 d117f78a

View on Github →

feat: port Topology.MetricSpace.Isometry (#2651)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Isometry.lean

added theorem Embedding.to_isometry

added theorem Isometry.antilipschitz

added theorem Isometry.closedEmbedding

added theorem Isometry.comp

added theorem Isometry.comp_continuousOn_iff

added theorem Isometry.comp_continuous_iff

added theorem Isometry.diam_image

added theorem Isometry.diam_range

added theorem Isometry.ediam_image

added theorem Isometry.ediam_range

added theorem Isometry.edist_eq

added def Isometry.isometryEquivOnRange

added theorem Isometry.lipschitz

added theorem Isometry.mapsTo_ball

added theorem Isometry.mapsTo_closedBall

added theorem Isometry.mapsTo_emetric_ball

added theorem Isometry.mapsTo_emetric_closedBall

added theorem Isometry.mapsTo_sphere

added theorem Isometry.preimage_ball

added theorem Isometry.preimage_closedBall

added theorem Isometry.preimage_emetric_ball

added theorem Isometry.preimage_emetric_closedBall

added theorem Isometry.preimage_setOf_dist

added theorem Isometry.preimage_sphere

added theorem Isometry.prod_map

added theorem Isometry.right_inv

added theorem Isometry.tendsto_nhds_iff

added def Isometry

added def IsometryEquiv.Simps.apply

added def IsometryEquiv.Simps.symm_apply

added theorem IsometryEquiv.apply_inv_self

added theorem IsometryEquiv.apply_symm_apply

added theorem IsometryEquiv.coe_eq_toEquiv

added theorem IsometryEquiv.coe_mk

added theorem IsometryEquiv.coe_mul

added theorem IsometryEquiv.coe_one

added theorem IsometryEquiv.coe_toEquiv

added theorem IsometryEquiv.coe_toHomeomorph

added theorem IsometryEquiv.coe_toHomeomorph_symm

added theorem IsometryEquiv.comp_continuousOn_iff

added theorem IsometryEquiv.comp_continuous_iff'

added theorem IsometryEquiv.comp_continuous_iff

added theorem IsometryEquiv.completeSpace_iff

added theorem IsometryEquiv.diam_image

added theorem IsometryEquiv.diam_preimage

added theorem IsometryEquiv.diam_univ

added theorem IsometryEquiv.ediam_image

added theorem IsometryEquiv.ediam_preimage

added theorem IsometryEquiv.ediam_univ

added theorem IsometryEquiv.eq_symm_apply

added theorem IsometryEquiv.ext

added theorem IsometryEquiv.image_ball

added theorem IsometryEquiv.image_closedBall

added theorem IsometryEquiv.image_emetric_ball

added theorem IsometryEquiv.image_emetric_closedBall

added theorem IsometryEquiv.image_sphere

added theorem IsometryEquiv.image_symm

added theorem IsometryEquiv.inv_apply_self

added def IsometryEquiv.mk'

added theorem IsometryEquiv.mul_apply

added theorem IsometryEquiv.preimage_ball

added theorem IsometryEquiv.preimage_closedBall

added theorem IsometryEquiv.preimage_emetric_ball

added theorem IsometryEquiv.preimage_emetric_closedBall

added theorem IsometryEquiv.preimage_sphere

added theorem IsometryEquiv.preimage_symm

added theorem IsometryEquiv.range_eq_univ

added theorem IsometryEquiv.self_comp_symm

added theorem IsometryEquiv.symm_apply_apply

added theorem IsometryEquiv.symm_apply_eq

added theorem IsometryEquiv.symm_comp_self

added theorem IsometryEquiv.symm_symm

added theorem IsometryEquiv.symm_trans_apply

added theorem IsometryEquiv.toEquiv_inj

added theorem IsometryEquiv.toEquiv_injective

added theorem IsometryEquiv.trans_apply

added structure IsometryEquiv

added theorem UniformEmbedding.to_isometry

added theorem isometry_dcomp

added theorem isometry_id

added theorem isometry_iff_dist_eq

added theorem isometry_iff_nndist_eq

added theorem isometry_subsingleton

added theorem isometry_subtype_coe