Theorem IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph

Modification history

2024-10-29 16:22

Mathlib/Topology/MetricSpace/Isometry.lean

feat: Homeomorphisms and IsometryEquivs based on `Equiv.piCongrLeft` and `Equiv.sumArrowEquivProdArrow` (#17981)

Added IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph View on Github →