liftZeroAtInfty — Mathlib

English

For a compact α, there is an equivalence between continuous maps α → β and vanishing-at-infinity continuous maps α → β.

Русский

Для компактного пространства α существует эквиваленция между непрерывными отображениями α → β и отображениями, исчезающими в бесконечности, α → β.

LaTeX

$$$ C(\alpha, \beta) \simeq C_0(\alpha, \beta) \quad (\alpha\text{ compact}). $$$

Lean4

/-- A continuous function on a compact space is automatically a continuous function vanishing at
infinity. -/
@[simps]
def liftZeroAtInfty [CompactSpace α] : C(α, β) ≃ C₀(α, β)
    where
  toFun
    f :=
    { toFun := f
      continuous_toFun := f.continuous
      zero_at_infty' := by simp }
  invFun f := f

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