support_subset — Mathlib

English

The support of each coordinate subset is contained in the dfinsupp support of x.

Русский

Опора (множество индексов с ненулевыми координатами) каждой координаты содержится в опоре dfinsupp x.

LaTeX

$$$$\\{\, i \mid (x_i : M) \\neq 0\,\\} \\subseteq \\operatorname{DFinsupp.support}(x).$$$$

Lean4

theorem support_subset [DecidableEq ι] [DecidableEq M] (A : ι → S) (x : DirectSum ι fun i => A i) :
    (Function.support fun i => (x i : M)) ⊆ ↑(DFinsupp.support x) :=
  by
  intro m
  simp only [Function.mem_support, Finset.mem_coe, DFinsupp.mem_support_toFun, not_imp_not, ZeroMemClass.coe_eq_zero,
    imp_self]

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