Commit 2026-05-02 21:31 e183c426
View on Github →feat(Topology/Homeomorph): add Equiv.IsHomeomorph_iff and LinearEquiv.IsHomeomorph_iff (#38660)
This PR adds two characterisations of IsHomeomorph for bundled equivalences. For a plain Equiv between topological spaces, Equiv.isHomeomorph_iff states that the equivalence is a homeomorphism if and only if it is continuous in both directions. The corresponding statement for a LinearEquiv between topological modules is added as LinearEquiv.isHomeomorph_iff, derived from the Equiv version.