Theorems · Definition · functional analysis

Distribution.IsVanishingOn

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

A distribution f vanishes on a set s if it vanishes for all test functions u with tsupport u ⊆ 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

27 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

FunLikeTopologicalSpaceZeroZero