toCocompactMap — Mathlib

English

A homeomorphism is a cocompact map.

Русский

Гомеоморфизм является кокомпактной отображением.

LaTeX

$$$\\text{Homeomorph}(\\alpha,\\beta) \\Rightarrow CocompactMap(\\alpha,\\beta)$$$

Lean4

/-- A homeomorphism is a cocompact map. -/
@[simps]
def toCocompactMap {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : CocompactMap α β
    where
  toFun := f
  continuous_toFun := f.continuous
  cocompact_tendsto' := by
    refine CocompactMap.tendsto_of_forall_preimage fun K hK => ?_
    have := K.preimage_equiv_eq_image_symm f.toEquiv
    simp only [coe_toEquiv] at this
    rw [this]
    exact hK.image f.symm.continuous

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