all_iff_forall_prop — Mathlib

English

Let l be a finite list of elements of a type α and p a predicate on α. Then p holds for every element of l if and only if, for every a, whenever a is in l, p(a) holds.

Русский

Пусть l — список элементов типа α, и p — предикат на α. Тогда p(a) верно для каждого элемента списка тогда и только тогда, когда для каждого a верно, что a ∈ l ⇒ p(a).

LaTeX

$$$$ (\forall a \in l,\ p(a)) \iff (\forall a,\ a \in l \rightarrow p(a)). $$$$

Lean4

theorem all_iff_forall_prop : (all l fun a => p a) ↔ ∀ a ∈ l, p a := by simp

Похожие утверждения