English
An element x belongs to the fold of supports iff there exists a function in the list whose support contains x.
Русский
Элемент x принадлежит свёртке опор тогда и только тогда, когда существует функция в списке, у которой опора содержит x.
LaTeX
$$$x \\in l.foldr(\\\\,\\\\text{support} \\\\u222a \\\\u00a0) \\\\emptyset \\\\iff \\\\exists f \\\\in l, x \\in f.\\\\operatorname{support}$$$
Lean4
theorem mem_foldr_sup_support_iff [Zero M] {l : List (ι →₀ M)} {x : ι} :
x ∈ l.foldr (Finsupp.support · ⊔ ·) ∅ ↔ ∃ f ∈ l, x ∈ f.support :=
by
simp only [Finset.sup_eq_union, Finsupp.mem_support_iff]
induction l with
| nil => simp
| cons hd tl IH => simp only [foldr, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH, mem_cons, exists_eq_or_imp]
