X : Type ?u.20432
α : Type u_1
α' : Type ?u.20438
β : Type ?u.20441
γ : Type ?u.20444
δ : Type ?u.20447
M : Type u_2
E : Type ?u.20453
R : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
X : Type ?u.20432
α : Type u_1
α' : Type ?u.20438
β : Type ?u.20441
γ : Type ?u.20444
δ : Type ?u.20447
M : Type u_2
E : Type ?u.20453
R : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x : α
hf : HasCompactSupport f'
⊢ HasCompactSupport (f • f')
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
no goals
X : Type ?u.20432
α : Type u_1
α' : Type ?u.20438
β : Type ?u.20441
γ : Type ?u.20444
δ : Type ?u.20447
M : Type u_2
E : Type ?u.20453
R : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
no goals
X : Type ?u.20432
α : Type u_1
α' : Type ?u.20438
β : Type ?u.20441
γ : Type ?u.20444
δ : Type ?u.20447
M : Type u_2
E : Type ?u.20453
R : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x✝ : α
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = OfNat.ofNat 0 x
⊢ (f • f') x = OfNat.ofNat 0 x
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]