genWeightSpace_le_genWeightSpaceOf

English

For any χ: L → R, weightSpace(M, χ) is included in genWeightSpace M χ; i.e., the classical weight space is contained in the generalized weight space for the same χ.

Русский

Для любого χ: L → R весовое пространство weightSpace(M, χ) включено в genWeightSpace M χ; то есть обычное весовое пространство содержится в обобщённом весовом пространстве по тем же χ.

LaTeX

$$$\\mathrm{weightSpace}(M, χ) \\subseteq \\mathrm{genWeightSpace}(M, χ)$$$

Lean4

theorem genWeightSpace_le_genWeightSpaceOf (x : L) (χ : L → R) : genWeightSpace M χ ≤ genWeightSpaceOf M (χ x) x :=
  iInf_le _ x

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