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)