chainTop — Mathlib

English

The last weight in the α-chain through β is the weight χ_top with value chainTopCoeff α β · α + β and nontrivial weight space.

Русский

Последний вес в α-цепочке через β — это вес χ_top со значением chainTopCoeff α β · α + β и ненулевым весовым пространством.

LaTeX

$$$ \\text{chainTop}(α, β) = (\\text{chainTopCoeff}(α, β) \\cdot α + β, \\; genWeightSpace\\ M(\\text{chainTopCoeff}(α, β) \\cdot α + β) ≠ ⊥) $$$

Lean4

/-- The last weight in an `α`-chain through `β`. -/
noncomputable def chainTop (α : L → R) (β : Weight R L M) : Weight R L M :=
  ⟨chainTopCoeff α β • α + β, genWeightSpace_nsmul_add_ne_bot_of_le α β le_rfl⟩

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