English
If an equivalence e: X ≃ Y preserves openness, i.e., for all subsets s of Y, IsOpen(e^{-1}(s)) ↔ IsOpen(s), then e is a homeomorphism.
Русский
Если равносильность e: X ≃ Y сохраняет открытость, т.е. для всех подмножеств s ⊆ Y выполняется IsOpen(e^{-1}(s)) ↔ IsOpen(s), то e является гомеоморфизмом.
LaTeX
$$$(\forall S \subseteq Y)\ IsOpen(e^{-1}(S)) \iff IsOpen(S) \Rightarrow e \text{ is a homeomorphism}.$$$
Lean4
/-- An equivalence between topological spaces respecting openness is a homeomorphism. -/
@[simps toEquiv]
def toHomeomorph (e : X ≃ Y) (he : ∀ s, IsOpen (e ⁻¹' s) ↔ IsOpen s) : X ≃ₜ Y
where
toEquiv := e
continuous_toFun := continuous_def.2 fun _ ↦ (he _).2
continuous_invFun := continuous_def.2 fun s ↦ by convert (he _).1; simp
