Theorems · Theorem · functional analysis

Filter.HasBasis.mem_dsupport

∀ {α : 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} {ι : Sort u_11} {p : ι → Prop} {s : ι → Set α} {x : α},
  (nhds x).HasBasis p s → (x ∈ Distribution.dsupport f ↔ ∀ (i : ι), p i → ¬Distribution.IsVanishingOn f (s i))

Defined in

Mathlib.Analysis.Distribution.Support

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeTopologicalSpaceZeroZero