Commit 2024-10-29 16:22 8d529992

View on Github →

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

Estimated changes

Modified Mathlib/Data/Fin/Tuple/Basic.lean

added theorem Fin.append_castAdd_natAdd

Modified Mathlib/Logic/Equiv/Fin.lean

added def Fin.appendEquiv

Modified Mathlib/Topology/Homeomorph.lean

added def Fin.appendHomeomorph

added theorem Fin.appendHomeomorph_toEquiv

added theorem Fin.continuous_append

added def Homeomorph.sumArrowHomeomorphProdArrow

Modified Mathlib/Topology/MetricSpace/Isometry.lean

added def Fin.appendIsometry

added theorem Fin.appendIsometry_toHomeomorph

added theorem Fin.edist_append_eq_max_edist

added def IsometryEquiv.piCongrLeft'

added def IsometryEquiv.piCongrLeft

added def IsometryEquiv.sumArrowIsometryEquivProdArrow

added theorem IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph