English
If s is a finite subset of indices and x is a family with coordinates in s, then the support of mk s x is contained in s.
Русский
Пусть s — конечное подмножество индексов, и x — семейство элементов с координатами в s. Тогда опора элемента mk s x лежит внутри s.
LaTeX
$$$\\operatorname{supp}(\\mathrm{mk}(s,x)) \\subseteq s$$$
Lean4
@[simp]
theorem support_mk_subset {s : Finset ι} {x : ∀ i : (↑s : Set ι), β i.1} : (mk s x).support ⊆ s := fun _ H =>
Multiset.mem_toFinset.1 (Finset.mem_filter.1 H).1