English
For any natural n with n ≤ chainTopCoeff α β, the weight space genWeightSpace M (n·α + β) is nontrivial (not equal to ⊥), provided α ≠ 0; if α = 0 this reduces to β's weight space being nontrivial.
Русский
Для любого натурального n с n ≤ chainTopCoeff α β весовое пространство genWeightSpace M (n·α + β) не равно ⊥ при условии α ≠ 0; если α = 0, то неравенство следует из β.
LaTeX
$$$ \\text{If } α ≠ 0, \\; n ≤ \\text{chainTopCoeff}(α, β) \\Rightarrow genWeightSpace M (n·α + β) \\neq ⊥. \\quad \\text{If } α = 0, \\; β \\text{ controls } genWeightSpace. $$$
Lean4
theorem genWeightSpace_nsmul_add_ne_bot_of_le {n} (hn : n ≤ chainTopCoeff α β) :
genWeightSpace M (n • α + β : L → R) ≠ ⊥ := by
by_cases hα : α = 0
· rw [hα, smul_zero, zero_add]; exact β.genWeightSpace_ne_bot
classical
rw [← Nat.lt_succ, Nat.succ_eq_add_one, chainTopCoeff_add_one _ _ hα] at hn
exact Nat.find_min (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists hn
