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.

Author: sharky564

Mathlib/Topology/Algebra/Module/Equiv.lean

@@ -1456,4 +1456,14 @@ theorem trans_smul [IsScalarTower S R G] (α : Sˣ) (e : G ≃L[R] V) (f : V ≃
     e.trans (α • f) = α • (e.trans f) := by ext; simp
 
 end ContinuousLinearEquiv
+
+/-- A linear equivalence between topological modules is a homeomorphism if and only if it is
+continuous in both directions. -/
+theorem LinearEquiv.isHomeomorph_iff {R S : Type*} [Semiring R] [Semiring S]
+    {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
+    {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [Module R M]
+    {N : Type*} [TopologicalSpace N] [AddCommMonoid N] [Module S N]
+    (e : M ≃ₛₗ[σ] N) : IsHomeomorph e ↔ Continuous e ∧ Continuous e.symm :=
+  e.toEquiv.isHomeomorph_iff
+
 end

Mathlib/Topology/Homeomorph/Lemmas.lean

@@ -514,6 +514,13 @@ lemma isHomeomorph_iff_exists_inverse : IsHomeomorph f ↔ Continuous f ∧ ∃
     exact ⟨h.symm, h.left_inv, h.right_inv, h.continuous_invFun⟩
   · exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph
 
+/-- An equivalence between topological spaces is a homeomorphism iff it is continuous in both
+directions. -/
+theorem Equiv.isHomeomorph_iff (e : X ≃ Y) :
+    IsHomeomorph e ↔ Continuous e ∧ Continuous e.symm := by
+  rw [e.continuous_symm_iff]
+  exact ⟨fun h ↦ ⟨h.continuous, h.isOpenMap⟩, fun ⟨hc, ho⟩ ↦ ⟨hc, ho, e.bijective⟩⟩
+
 /-- A map is a homeomorphism iff it is a surjective embedding. -/
 lemma isHomeomorph_iff_isEmbedding_surjective : IsHomeomorph f ↔ IsEmbedding f ∧ Surjective f where
   mp hf := ⟨hf.isEmbedding, hf.surjective⟩