genWeightSpace_le_genWeightSpaceChain

English

For any k with k ∈ Ioo(p,q), genWeightSpace(k χ1 + χ2) ≤ genWeightSpaceChain M χ1 χ2 p q.

Русский

Для любого k ∈ Ioo(p,q) весовое пространство genWeightSpace(k χ1 + χ2) содержится в genWeightSpaceChain M χ1 χ2 p q.

LaTeX

$$$\forall k \in Ioo(p,q),\ genWeightSpace(M, k \cdot χ_1 + χ_2) \le genWeightSpaceChain(M, χ_1, χ_2, p, q)$$$

Lean4

theorem genWeightSpace_le_genWeightSpaceChain {k : ℤ} (hk : k ∈ Ioo p q) :
    genWeightSpace M (k • χ₁ + χ₂) ≤ genWeightSpaceChain M χ₁ χ₂ p q :=
  le_biSup (fun i ↦ genWeightSpace M (i • χ₁ + χ₂)) hk

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