Commit 2022-04-06 06:48 6930ad5d

feat(topology/continuous_function/zero_at_infty): add the type of continuous functions vanishing at infinity (#12907) This adds the type of of continuous functions vanishing at infinity (zero_at_infty) with the localized notation C₀(α, β) (we also allow α →C₀ β but the former has higher priority). This type is defined when α and β are topological spaces and β has a zero element. Elements of this type are continuous functions f with the additional property that tendsto f (cocompact α) (𝓝 0). Here we attempt to follow closely the recent hom refactor and so we also create the type class zero_at_infty_continuous_map_class. Various algebraic structures are instantiated on C₀(α, β) when corresponding structures exist on β. When β is a metric space, there is a natural inclusion zero_at_infty_continuous_map.to_bcf : C₀(α, β) → α →ᵇ β, which induces a metric space structure on C₀(α, β), and the range of this map is closed. Therefore, when β is complete, α →ᵇ β is complete, and hence so is C₀(α, β).

• depends on: #12894