forall_iff_forall_mem — Mathlib

English

Forall p l is equivalent to saying that p holds for every element of l.

Русский

Forall p l эквивалентно тому, что p верно для каждого элемента списка l.

LaTeX

$$$ \\forall {l : List\\, \\alpha},\\ Forall\\ p\\ l \\iff \\forall x\\in l,\\ p\\ x $$$

Lean4

theorem forall_iff_forall_mem : ∀ {l : List α}, Forall p l ↔ ∀ x ∈ l, p x
  | [] => (iff_true_intro <| forall_mem_nil _).symm
  | x :: l => by rw [forall_mem_cons, forall_cons, forall_iff_forall_mem]

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