Boolean quantifiers

This proves a few properties about List.all and List.any, which are the Bool universal and existential quantifiers. Their definitions are in core Lean.

@[deprecated List.all_eq_true (since := "2024-08-10")]

theorem List.all_iff_forall {α : Type u_1} {p : α → Bool} {l : List α} : l.all p = true ↔ ∀ (x : α), x ∈ l → p x = true

Alias of List.all_eq_true.

theorem List.all_iff_forall_prop {α : Type u_1} {p : α → Prop} [DecidablePred p] {l : List α} : (l.all fun (a : α) => decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a

@[deprecated List.any_eq_true (since := "2024-08-10")]

theorem List.any_iff_exists {α : Type u_1} {p : α → Bool} {l : List α} : l.any p = true ↔ ∃ (x : α), x ∈ l ∧ p x = true

Alias of List.any_eq_true.

theorem List.any_iff_exists_prop {α : Type u_1} {p : α → Prop} [DecidablePred p] {l : List α} : (l.any fun (a : α) => decide (p a)) = true ↔ ∃ (a : α), a ∈ l ∧ p a

theorem List.any_of_mem {α : Type u_1} {l : List α} {a : α} {p : α → Bool} (h₁ : a ∈ l) (h₂ : p a = true) : l.any p = true