mathlib documentation

data.bool.all_any

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.

@[simp]
theorem list.all_nil {α : Type u_1} (p : α → bool) :
@[simp]
theorem list.all_cons {α : Type u_1} (p : α → bool) (a : α) (l : list α) :
(a :: l).all p = p a && l.all p
theorem list.all_iff_forall {α : Type u_1} {l : list α} {p : α → bool} :
(l.all p) ∀ (a : α), a l(p a)
theorem list.all_iff_forall_prop {α : Type u_1} {p : α → Prop} [decidable_pred p] {l : list α} :
(l.all (λ (a : α), decidable.to_bool (p a))) ∀ (a : α), a lp a
@[simp]
theorem list.any_nil {α : Type u_1} (p : α → bool) :
@[simp]
theorem list.any_cons {α : Type u_1} (p : α → bool) (a : α) (l : list α) :
(a :: l).any p = p a || l.any p
theorem list.any_iff_exists {α : Type u_1} {l : list α} {p : α → bool} :
(l.any p) ∃ (a : α) (H : a l), (p a)
theorem list.any_iff_exists_prop {α : Type u_1} {p : α → Prop} [decidable_pred p] {l : list α} :
(l.any (λ (a : α), decidable.to_bool (p a))) ∃ (a : α) (H : a l), p a
theorem list.any_of_mem {α : Type u_1} {l : list α} {a : α} {p : α → bool} (h₁ : a l) (h₂ : (p a)) :
(l.any p)