English
Let p be a predicate on α. For any a ∈ α and any multiset s of α, the statement “p holds for all x in a ::ₘ s” is equivalent to “p holds for a and p holds for all x in s.”
Русский
Пусть p — предикат на α. Для любого a ∈ α и множества-мультимножества s справедливо: p(x) верно для всех x из a ::ₘ s тогда и только тогда, когда p(a) верно и p(x) верно для всех x из s.
LaTeX
$$$\\forall p:\\alpha \\to \\mathrm{Prop},\\ a:\\alpha,\\ s:\\mathrm{Multiset}\\alpha,\\ (\\forall x \\in a ::ₘ s,\\ p\\,x) \\leftrightarrow (p\\,a \\land \\forall x \\in s,\\ p\\,x)$$$
Lean4
theorem forall_mem_cons {p : α → Prop} {a : α} {s : Multiset α} : (∀ x ∈ a ::ₘ s, p x) ↔ p a ∧ ∀ x ∈ s, p x :=
Quotient.inductionOn' s fun _ => List.forall_mem_cons
