disjoint_genWeightSpace — Mathlib

English

The family of weight spaces {genWeightSpace M χ} is independent as χ ranges over all weights.

Русский

Семейство весовых пространств {genWeightSpace(M, χ)} независимо при вариации χ.

LaTeX

$$iSupIndep (fun χ => genWeightSpace M χ)$$

Lean4

theorem disjoint_genWeightSpace [NoZeroSMulDivisors R M] {χ₁ χ₂ : L → R} (h : χ₁ ≠ χ₂) :
    Disjoint (genWeightSpace M χ₁) (genWeightSpace M χ₂) :=
  by
  obtain ⟨x, hx⟩ : ∃ x, χ₁ x ≠ χ₂ x := Function.ne_iff.mp h
  exact
    (disjoint_genWeightSpaceOf R L M hx).mono (genWeightSpace_le_genWeightSpaceOf M x χ₁)
      (genWeightSpace_le_genWeightSpaceOf M x χ₂)

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