α : Type u_2
β : Type u_1
M : Type ?u.7467
E : Type ?u.7470
inst✝ : Zero β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 0
⊢ Set.indicator s 0 =ᶠ[l] 0
α : Type u_2
β : Type u_1
M : Type ?u.7467
E : Type ?u.7470
inst✝ : Zero β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 0
⊢ Set.indicator s f =ᶠ[l] 0
refine' hf.indicator.trans _
no goals
α : Type u_2
β : Type u_1
M : Type ?u.7467
E : Type ?u.7470
inst✝ : Zero β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 0
⊢ Set.indicator s 0 =ᶠ[l] 0
rw [indicator_zero']