continuous_symm_of_equiv_compact_to_t2

English

If X is compact and Y is Hausdorff and f: X ≃ Y is continuous, then the inverse map f^{-1} is continuous.

Русский

Если X компактно, Y удовлетворяет свойству Т2 и f: X ≃ Y непрерывно, то обратное отображение f^{-1} непрерывно.

LaTeX

$$$\mathrm{Continuous}(f) \Rightarrow \mathrm{Continuous}(f^{-1})$$$

Lean4

theorem continuous_symm_of_equiv_compact_to_t2 [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous f) :
    Continuous f.symm := by
  rw [continuous_iff_isClosed]
  intro C hC
  have hC' : IsClosed (f '' C) := (hC.isCompact.image hf).isClosed
  rwa [Equiv.image_eq_preimage] at hC'

Похожие утверждения