Theorems · Inductive type · general topology

ZeroAtInftyContinuousMap

(α : Type u) → (β : Type v) → [TopologicalSpace α] → [Zero β] → [TopologicalSpace β] → Type (max u v)

C₀(α, β) is the type of continuous functions α → β which vanish at infinity from a topological space to a metric space with a zero element. When possible, instead of parametrizing results over (f : C₀(α, β)), you should parametrize over (F : Type*) [ZeroAtInftyContinuousMapClass F α β] (f : F). When you extend this structure, make sure to extend ZeroAtInftyContinuousMapClass.

Defined in

Mathlib.Topology.ContinuousMap.ZeroAtInfty

Cited by

47 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceZeroTopologicalSpace