X : Type ?u.28023
α : Type u_1
α' : Type ?u.28029
β : Type ?u.28032
γ : Type ?u.28035
δ : Type ?u.28038
M : Type u_2
E : Type ?u.28044
R : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
X : Type ?u.28023
α : Type u_1
α' : Type ?u.28029
β : Type ?u.28032
γ : Type ?u.28035
δ : Type ?u.28038
M : Type u_2
E : Type ?u.28044
R : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : HasCompactSupport f'
⊢ HasCompactSupport (f • f')
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
no goals
X : Type ?u.28023
α : Type u_1
α' : Type ?u.28029
β : Type ?u.28032
γ : Type ?u.28035
δ : Type ?u.28038
M : Type u_2
E : Type ?u.28044
R : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
refine' hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
no goals
X : Type ?u.28023
α : Type u_1
α' : Type ?u.28029
β : Type ?u.28032
γ : Type ?u.28035
δ : Type ?u.28038
M : Type u_2
E : Type ?u.28044
R : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero 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]