weightedHomogeneousComponent_finsupp

English

The set of degrees m for which the weighted homogeneous component is defined forms a finite set; equivalently, the function m ↦ weightedHomogeneousComponent w m φ has finite support.

Русский

Множество степеней m, для которых определена взвешенная однородная компонента, является конечным; иначе говоря, поддержка функции m ↦ weightedHomogeneousComponent w m φ конечна.

LaTeX

$$$\operatorname{Finite}(\operatorname{supp}(\phi)) \Rightarrow (\operatorname{support}(m \mapsto weightedHomogeneousComponent w m \phi)\ is\ finite)$$$

Lean4

theorem weightedHomogeneousComponent_finsupp : (Function.support fun m => weightedHomogeneousComponent w m φ).Finite :=
  by
  apply ((fun d : σ →₀ ℕ => (weight w) d) '' (φ.support : Set (σ →₀ ℕ))).toFinite.subset
  intro m hm
  by_contra hm'
  apply hm (weightedHomogeneousComponent_eq_zero' m φ _)
  simpa only [Set.mem_image, not_exists, not_and] using hm'

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