support_mk_subset — Mathlib

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

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