mathlib3 documentation

data.bool.all_any

Boolean quantifiers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 l p 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)