Theorems · Theorem · general topology

ZeroAtInftyContinuousMap.zeroAtInftyContinuousMapClass.ofCompact

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β] {G : Type u_2}
  [inst_3 : FunLike G α β] [ContinuousMapClass G α β] [CompactSpace α], ZeroAtInftyContinuousMapClass G α β

A continuous function on a compact space is automatically a continuous function vanishing at infinity. This is not an instance to avoid type class loops.

Defined in

Mathlib.Topology.ContinuousMap.ZeroAtInfty

Cited by

0 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceZeroFunLikeContinuousMapClassCompactSpace