Theorems · Theorem · functional analysis

CompactlySupportedContinuousMapClass.of_compactSpace

∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (G : Type u_5) [inst_3 : FunLike G α β] [ContinuousMapClass G α β] [CompactSpace α],
  CompactlySupportedContinuousMapClass G α β

A continuous function on a compact space has automatically compact support. This is not an instance to avoid type class loops.

Defined in

Mathlib.Topology.ContinuousMap.CompactlySupported

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceZeroTopologicalSpaceFunLikeContinuousMapClassCompactSpace