Theorems · Definition · general topology

HasCompactMulSupport

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

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

Defined in

Mathlib.Topology.Algebra.Support

Cited by

43 results in Mathlib

Foundations

Depth 50 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceOne