Theorems · Inductive type · functional analysis

CompactlySupportedContinuousMap

(α : Type u_5) → (β : Type u_6) → [TopologicalSpace α] → [Zero β] → [TopologicalSpace β] → Type (max u_5 u_6)

C_c(α, β) is the type of continuous functions α → β with compact support from a topological space to a topological space with a zero element. When possible, instead of parametrizing results over f : C_c(α, β), you should parametrize over {F : Type*} [CompactlySupportedContinuousMapClass F α β] (f : F). When you extend this structure, make sure to extend CompactlySupportedContinuousMapClass.

Defined in

Mathlib.Topology.ContinuousMap.CompactlySupported

Cited by

134 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

TopologicalSpaceZeroTopologicalSpace