Documentation

Mathlib.Data.Bool.AllAny

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.

theorem List.all_iff_forall {α : Type u_1} {l : List α} {p : αBool} :
l.all p = true ∀ (a : α), a lp a = 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 lp a
theorem List.any_iff_exists {α : Type u_1} {l : List α} {p : αBool} :
l.any p = true ∃ (a : α), a l p a = 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