Theorems · Theorem · functional analysis

Distribution.mem_dsupport_iff_frequently

∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} {x : α},
  x ∈ Distribution.dsupport f ↔ ∃ᶠ (u : Set α) in (nhds x).smallSets, ¬Distribution.IsVanishingOn f u

Defined in

Mathlib.Analysis.Distribution.Support

Cited by

1 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FunLikeTopologicalSpaceZeroZero