α : Type u_1
l : List α
p q : α → Bool
⊢ (∃ a, a ∈ l ∧ p a = true) ↔ ¬∀ (a : α), a ∈ l → ¬p a = true
α : Type u_1
l : List α
p q : α → Bool
⊢ countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true
rw [← not_iff_not, ← Ne.def, ← pos_iff_ne_zero, countp_pos]
no goals
α : Type u_1
l : List α
p q : α → Bool
⊢ (∃ a, a ∈ l ∧ p a = true) ↔ ¬∀ (a : α), a ∈ l → ¬p a = true
simp