sigmaFinsuppEquivDFinsupp_support

English

The support of the constructed DFinsupp equivalence equals the split support of f: the indices where f has nonzero components correspond exactly to the sigma-structure's support.

Русский

Поддержка построенного эквивалента DFinsupp равна splitSupport f: индексы, на которых f имеет ненулевые компоненты, совпадают с поддержкой сигма-структуры.

LaTeX

$$$ (sigmaFinsuppEquivDFinsupp f).\\text{support} = Finsupp.splitSupport f $$$

Lean4

@[simp]
theorem sigmaFinsuppEquivDFinsupp_support [DecidableEq ι] [Zero N] [∀ (i : ι) (x : η i →₀ N), Decidable (x ≠ 0)]
    (f : (Σ i, η i) →₀ N) : (sigmaFinsuppEquivDFinsupp f).support = Finsupp.splitSupport f :=
  by
  ext
  rw [DFinsupp.mem_support_toFun]
  exact (Finsupp.mem_splitSupport_iff_nonzero _ _).symm

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