Theorems · Definition · general topology

HasCompactSupport

{α : Type u_2} → {β : Type u_4} → [TopologicalSpace α] → [Zero β] → (α → β) → Prop

A function f has compact support or is compactly supported if the closure of the support of f is compact. In a T₂ space this is equivalent to f being equal to 0 outside a compact set.

Defined in

Mathlib.Topology.Algebra.Support

Cited by

196 results in Mathlib

Foundations

Depth 50 from the axioms, rests on 550 definitions · uses propext, Quot.sound

Assumes

TopologicalSpaceZero