X : Type ?u.26610
α : Type u_1
α' : Type ?u.26616
β : Type ?u.26619
γ : Type ?u.26622
δ : Type ?u.26625
M : Type u_3
E : Type ?u.26631
R : Type u_2
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.26610
α : Type u_1
α' : Type ?u.26616
β : Type ?u.26619
γ : Type ?u.26622
δ : Type ?u.26625
M : Type u_3
E : Type ?u.26631
R : Type u_2
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.26610
α : Type u_1
α' : Type ?u.26616
β : Type ?u.26619
γ : Type ?u.26622
δ : Type ?u.26625
M : Type u_3
E : Type ?u.26631
R : Type u_2
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
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]
no goals
X : Type ?u.26610
α : Type u_1
α' : Type ?u.26616
β : Type ?u.26619
γ : Type ?u.26622
δ : Type ?u.26625
M : Type u_3
E : Type ?u.26631
R : Type u_2
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, zero_smul]