finite_support — Mathlib

English

For any element x of the direct sum, the support set of its coordinates is finite.

Русский

Для любого элемента x в прямой сумме множество опор координат конечное.

LaTeX

$$$$\\operatorname{Finite}\\big(\\operatorname{support}(i \\mapsto (x_i : M))\\big).$$$$

Lean4

theorem finite_support (A : ι → S) (x : DirectSum ι fun i => A i) : (Function.support fun i => (x i : M)).Finite := by
  classical exact (DFinsupp.support x).finite_toSet.subset (DirectSum.support_subset _ x)

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