Theorems · Theorem · general topology

Function.locallyFinsuppWithin.nsmul_posPart

∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y]
  [inst_2 : LinearOrder Y] [IsOrderedAddMonoid Y] (n : ℕ) (f : Function.locallyFinsuppWithin U Y), (n • f)⁺ = n • f⁺

Taking the positive part of a function with locally finite support commutes with scalar multiplication by a natural number.

Defined in

Mathlib.Topology.LocallyFinsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommGroupLinearOrderIsOrderedAddMonoid