isoOfTopologicalSpace — Mathlib

Lean4

/-- This definition is used to prove essential surjectivity of `compactumToCompHaus`. -/
noncomputable def isoOfTopologicalSpace {D : CompHaus} : compactumToCompHaus.obj (Compactum.ofTopologicalSpace D) ≅ D
    where
  hom :=
    CompHausLike.ofHom _
      { toFun := id
        continuous_toFun :=
          continuous_def.2 fun _ h => by
            rw [isOpen_iff_ultrafilter'] at h
            exact h }
  inv :=
    CompHausLike.ofHom _
      { toFun := id
        continuous_toFun :=
          continuous_def.2 fun _ h1 => by
            rw [isOpen_iff_ultrafilter']
            intro _ h2
            exact h1 _ h2 }

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