Commit 2024-01-26 18:21 edd8f405

View on Github →

feat: link Dilation to Isometry and Homeomorph (#9980)

Estimated changes

Modified Mathlib/Topology/MetricSpace/Dilation.lean

added def Isometry.toDilation

added theorem Isometry.toDilation_ratio

Modified Mathlib/Topology/MetricSpace/DilationEquiv.lean

added theorem DilationEquiv.coe_toHomeomorph

added theorem DilationEquiv.ratio_toDilation

added def DilationEquiv.toHomeomorph

added theorem DilationEquiv.toHomeomorph_symm

added def IsometryEquiv.toDilationEquiv

added theorem IsometryEquiv.toDilationEquiv_apply

added theorem IsometryEquiv.toDilationEquiv_ratio

added theorem IsometryEquiv.toDilationEquiv_symm

added theorem IsometryEquiv.toDilationEquiv_toDilation