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.

source
@[simp]
theorem list.all_nil {α : Type u_1} (p : α → bool) :
list.nil.all p = bool.tt
source
@[simp]
theorem list.all_cons {α : Type u_1} (p : α → bool) (a : α) (l : list α) :
(a :: l).all p = p a && l.all p
source
theorem list.all_iff_forall {α : Type u_1} {l : list α} {p : α → bool} :
↥(l.all p) ↔ ∀ (a : α), a ∈ l → ↥(p a)
source
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
source
@[simp]
theorem list.any_nil {α : Type u_1} (p : α → bool) :
list.nil.any p = bool.ff
source
@[simp]
theorem list.any_cons {α : Type u_1} (p : α → bool) (a : α) (l : list α) :
(a :: l).any p = p a || l.any p
source
theorem list.any_iff_exists {α : Type u_1} {l : list α} {p : α → bool} :
↥(l.any p) ↔ ∃ (a : α) (H : a ∈ l), ↥(p a)
source
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
source
theorem list.any_of_mem {α : Type u_1} {l : list α} {a : α} {p : α → bool} (h₁ : a ∈ l) (h₂ : ↥(p a)) :
↥(l.any p)
source
@[protected, instance]
def list.decidable_forall_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] (l : list α) :
decidable (∀ (x : α), x ∈ l → p x)
Equations
source
@[protected, instance]
def list.decidable_exists_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] (l : list α) :
decidable (∃ (x : α) (H : x ∈ l), p x)
Equations