Finset.mem_finsupp_iff_of_support_subset

theorem Finset.mem_finsupp_iff_of_support_subset : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] {s : Finset ι} {f : ι →₀ α} {t : ι →₀ Finset α}, t.support ⊆ s → (f ∈ s.finsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i)

The theorem `Finset.mem_finsupp_iff_of_support_subset` states that for any types `ι` and `α` where `α` is a type with zero, any `Finset` `s` of type `ι`, any function `f` from type `ι` to `α` (with finite support), and another function `t` from type `ι` to `Finset` of `α`, if the support of `t` is a subset of `s`, then `f` is in the `finsupp` (the set of functions with finite support) of `s` applied to `t` if and only if for every `i` of type `ι`, the value of `f` at `i` is an element of the `Finset` given by `t` at `i`.

More concisely: For any type `ι`, function `f` from `ι` to type `α` with finite support, `Finset` `s` of type `ι`, and function `t` from `ι` to `Finset` of `α` with support subset of `s`, `f` is in the `finsupp` of `s` applied to `t` if and only if for all `i` in `s`, `f i` is an element of `t i`.