support_mk'_subset — Mathlib

English

For a function f and a multiset s with a witness h that f i = 0 outside s, the support of mk' f (Trunc.mk ⟨s,h⟩) is contained in s.toFinset.

Русский

Для функции f и мультисета s с доказательством h, что f i = 0 вне s, опора mk' f (Trunc.mk ⟨s,h⟩) лежит внутри s.toFinset.

LaTeX

$$$\\operatorname{supp}(\\mathrm{mk}' f \\; \\mathrm{Trunc.mk} ⟨s,h⟩) \\subseteq s^{\\mathrm{toFinset}}$$$

Lean4

@[simp]
theorem support_mk'_subset {f : ∀ i, β i} {s : Multiset ι} {h} : (mk' f <| Trunc.mk ⟨s, h⟩).support ⊆ s.toFinset :=
  fun i H => Multiset.mem_toFinset.1 <| by simpa using (Finset.mem_filter.1 H).1

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