Theorems · Theorem · general topology

Function.locallyFinsuppWithin.sum_apply_smul_single_eq_self

∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : DecidableEq X] [inst_2 : AddCommMonoid Y]
  {U : Set X} {F : Function.locallyFinsuppWithin U Y},
  F.support.Finite →
    ∑ᶠ (x : X), Function.locallyFinsuppWithin.restrict (Function.locallyFinsuppWithin.single x (F x)) ⋯ = F

Present a function with with finite support as a finsum of singleton indicator functions.

Defined in

Mathlib.Topology.LocallyFinsupp

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDecidableEqAddCommMonoid