Theorems · Definition · functional analysis

Distribution.dsupport

{α : Type u_2} →
  {β : Type u_3} →
    {F : Type u_6} → {V : Type u_10} → [FunLike F α β] → [TopologicalSpace α] → [Zero β] → [Zero V] → (F → V) → Set α

The distributional support of f is the intersection of all closed sets s such that f vanishes on the complement of s. To make this definition work for all types of distributions, we define it for any function from a FunLike type to a type with zero.

Defined in

Mathlib.Analysis.Distribution.Support

Cited by

21 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

FunLikeTopologicalSpaceZeroZero