isIso_of_bijective — Mathlib

English

A continuous bijection between compact Hausdorff spaces is an isomorphism.

Русский

Непрерывное биективное отображение между компактно-хаусдорфовыми пространствами является изоморфизмом.

LaTeX

$$$\forall {P},{X,Y : CompHausLike P},\ f:\,X \to Y,\ \text{Bijective}(f) \Rightarrow \mathrm{IsIso}(f)$$$

Lean4

/-- Any continuous bijection of compact Hausdorff spaces is an isomorphism. -/
theorem isIso_of_bijective {X Y : CompHausLike.{u} P} (f : X ⟶ Y) (bij : Function.Bijective f) : IsIso f :=
  by
  let E := Equiv.ofBijective _ bij
  have hE : Continuous E.symm := by
    rw [continuous_iff_isClosed]
    intro S hS
    rw [← E.image_eq_preimage]
    exact isClosedMap f S hS
  refine ⟨⟨ofHom _ ⟨E.symm, hE⟩, ?_, ?_⟩⟩
  · ext x
    apply E.symm_apply_apply
  · ext x
    apply E.apply_symm_apply

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