Commit 2023-09-06 10:25 b550667f

View on Github →

feat: Strengthening an equiv to an homeo (#6980) Add Equiv.toHomeomorph, a convenient version of Equiv.toHomeomorph_of_inducing.

Estimated changes

Modified Mathlib/Topology/Homeomorph.lean

added theorem Equiv.coe_toHomeomorph

added def Equiv.toHomeomorph

modified def Equiv.toHomeomorphOfInducing

added theorem Equiv.toHomeomorph_apply

added theorem Equiv.toHomeomorph_refl

added theorem Equiv.toHomeomorph_symm

added theorem Equiv.toHomeomorph_trans