α : Type u_1
β : Type ?u.22547
γ : Type ?u.22550
ι : Type ?u.22553
M : Type u_2
M' : Type ?u.22559
N : Type ?u.22562
P : Type ?u.22565
G : Type ?u.22568
H : Type ?u.22571
R : Type ?u.22574
S : Type ?u.22577
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ (∀ (x : α), ↑f x ≠ 0 → x ∈ s) ↔ ∀ (a : α), ¬a ∈ s → ↑f a = 0
α : Type u_1
β : Type ?u.22547
γ : Type ?u.22550
ι : Type ?u.22553
M : Type u_2
M' : Type ?u.22559
N : Type ?u.22562
P : Type ?u.22565
G : Type ?u.22568
H : Type ?u.22571
R : Type ?u.22574
S : Type ?u.22577
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ ↑f.support ⊆ s ↔ ∀ (a : α), ¬a ∈ s → ↑f a = 0
simp only [Set.subset_def, mem_coe, mem_support_iff]
no goals
α : Type u_1
β : Type ?u.22547
γ : Type ?u.22550
ι : Type ?u.22553
M : Type u_2
M' : Type ?u.22559
N : Type ?u.22562
P : Type ?u.22565
G : Type ?u.22568
H : Type ?u.22571
R : Type ?u.22574
S : Type ?u.22577
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ (∀ (x : α), ↑f x ≠ 0 → x ∈ s) ↔ ∀ (a : α), ¬a ∈ s → ↑f a = 0
exact forall_congr' fun a => not_imp_comm