chore: a missing List lemma in Init (#3344)

This commit is contained in:
Scott Morrison 2024-02-15 19:55:48 +11:00 committed by GitHub
parent 9a3f0f1909
commit ae524d465f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -418,8 +418,8 @@ theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
· exact or_congr_left (and_iff_left_of_imp fun | rfl => h).symm
· exact (or_iff_right fun ⟨rfl, h'⟩ => h h').symm
-- theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by
-- simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by
simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
/-! ### findSome? -/