Skip to content

Commit 5821f8c

Browse files
grunwegocfnash
andcommitted
feat: add LocallyFinite.smul_{left,right} (#10020)
From sphere-eversion. Will be used to show a point-wise version of `SmoothPartitionOfUnity.contMDiff_finsum_smul`. Co-authored-by: Oliver Nash <github@olivernash.org>
1 parent e165098 commit 5821f8c

File tree

1 file changed

+10
-0
lines changed

1 file changed

+10
-0
lines changed

Mathlib/Topology/Support.lean

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -420,4 +420,14 @@ theorem locallyFinite_mulSupport_iff [CommMonoid M] {f : ι → X → M} :
420420
(LocallyFinite fun i ↦ mulSupport <| f i) ↔ LocallyFinite fun i ↦ mulTSupport <| f i :=
421421
⟨LocallyFinite.closure, fun H ↦ H.subset fun _ ↦ subset_closure⟩
422422

423+
theorem LocallyFinite.smul_left [Zero R] [Zero M] [SMulWithZero R M]
424+
{s : ι → X → R} (h : LocallyFinite fun i ↦ support <| s i) (f : ι → X → M) :
425+
LocallyFinite fun i ↦ support <| s i • f i :=
426+
h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, zero_smul]
427+
428+
theorem LocallyFinite.smul_right [Zero M] [SMulZeroClass R M]
429+
{f : ι → X → M} (h : LocallyFinite fun i ↦ support <| f i) (s : ι → X → R) :
430+
LocallyFinite fun i ↦ support <| s i • f i :=
431+
h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, smul_zero]
432+
423433
end LocallyFinite

0 commit comments

Comments
 (0)