equivSetOf — Mathlib

English

There is a natural equivalence between the set of weights and the subtype of functions whose associated weight space is nontrivial.

Русский

Существует естественное эквивалентное отображение между множеством весов и подмножеством функций, для которых веcтовое пространство непусто.

LaTeX

$$equiv (LieModule.Weight R L M) { χ : L → R | genWeightSpace M χ ≠ ⊥ }$$

Lean4

/-- The set of weights is equivalent to a subtype. -/
def equivSetOf : Weight R L M ≃ {χ : L → R | genWeightSpace M χ ≠ ⊥}
    where
  toFun w := ⟨w.1, w.2⟩
  invFun w := ⟨w.1, w.2⟩
  left_inv w := by simp
  right_inv w := by simp

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