coeff_isPWOsupport — Mathlib

English

For A ∈ HVertexOperator and v ∈ V, the function giving coefficients of (A v) has partially well-ordered support.

Русский

Для A ∈ HVertexOperator и v ∈ V множество индексов, при которых коэффициенты ненулевые в (A v), образует частично упорядоченное множество.

LaTeX

$$$\\text{IsPWO}\\bigl(\\operatorname{support}(\\text{coeff}(A v))\\bigr)$$$

Lean4

theorem coeff_isPWOsupport (A : HVertexOperator Γ R V W) (v : V) : ((of R).symm (A v)).coeff.support.IsPWO :=
  ((of R).symm (A v)).isPWO_support'

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