X : Type ?u.31932
α : Type u_1
α' : Type ?u.31938
β : Type u_2
γ : Type ?u.31944
δ : Type ?u.31947
M : Type ?u.31950
E : Type ?u.31953
R : Type ?u.31956
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0
X : Type ?u.31932
α : Type u_1
α' : Type ?u.31938
β : Type u_2
γ : Type ?u.31944
δ : Type ?u.31947
M : Type ?u.31950
E : Type ?u.31953
R : Type ?u.31956
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : HasCompactSupport f'
⊢ HasCompactSupport (f * f')
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
no goals
X : Type ?u.31932
α : Type u_1
α' : Type ?u.31938
β : Type u_2
γ : Type ?u.31944
δ : Type ?u.31947
M : Type ?u.31950
E : Type ?u.31953
R : Type ?u.31956
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0
refine' hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]
no goals
X : Type ?u.31932
α : Type u_1
α' : Type ?u.31938
β : Type u_2
γ : Type ?u.31944
δ : Type ?u.31947
M : Type ?u.31950
E : Type ?u.31953
R : Type ?u.31956
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x✝ : α
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = OfNat.ofNat 0 x
⊢ (f * f') x = OfNat.ofNat 0 x
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]