Theorems · Theorem · general topology

Function.locallyFinsuppWithin.coe_finsum

∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {ι : Type u_3} {F : ι → Function.locallyFinsuppWithin U ℤ},
  ⇑(∑ᶠ (i : ι), F i) = ∑ᶠ (i : ι), ⇑(F i)

Defined in

Mathlib.Topology.LocallyFinsupp

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace