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_prop
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{l : list α} :
↥(l.all (λ (a : α), decidable.to_bool (p a))) ↔ ∀ (a : α), 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
@[protected, instance]
Equations
- l.decidable_forall_mem = decidable_of_iff ↥(l.all (λ (a : α), decidable.to_bool (p a))) _
@[protected, instance]
Equations
- l.decidable_exists_mem = decidable_of_iff ↥(l.any (λ (a : α), decidable.to_bool (p a))) _