Theorems · Inductive type · general topology

ZeroAtInftyContinuousMapClass

(F : Type u_2) →
  (α : outParam (Type u_3)) →
    (β : outParam (Type u_4)) → [TopologicalSpace α] → [Zero β] → [TopologicalSpace β] → [FunLike F α β] → Prop

ZeroAtInftyContinuousMapClass F α β states that F is a type of continuous maps which vanish at infinity. You should also extend this typeclass when you extend ZeroAtInftyContinuousMap.

Defined in

Mathlib.Topology.ContinuousMap.ZeroAtInfty

Cited by

5 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

TopologicalSpaceZeroTopologicalSpaceFunLike