Theorem IsometryClass.toIsometryEquiv_injective

Modification history

2025-05-09 19:38
Mathlib/Topology/MetricSpace/Isometry.lean
feat: `IsometryClass` (#18754)
Added IsometryClass.toIsometryEquiv_injectiveView on Github →