LocallyConstant.congrLeftₐ.proof_1

theorem LocallyConstant.congrLeftₐ.proof_1 : ∀ {X : Type u_2} {Y : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y), Continuous ⇑e.symm

This theorem, `LocallyConstant.congrLeftₐ.proof_1`, states that for all types `X` and `Y`, where both `X` and `Y` are equipped with a topological space structure (symbolized by `TopologicalSpace X` and `TopologicalSpace Y`), if there exists a homeomorphism `e` from `X` to `Y`, then the inverse function of `e` is continuous. The inverse function is obtained by applying the `Homeomorph.symm` operation to `e`. In mathematical terms, given a homeomorphism $\approx_t : X \rightarrow Y$, its inverse $\approx_t^{-1} : Y \rightarrow X$ is always continuous.

More concisely: If `X` and `Y` are topological spaces with a homeomorphism `e : X ≈ Y`, then the inverse `e⁻¹` of `e` is a continuous function from `Y` to `X`.