mem_posFittingCompOf — Mathlib

English

There is an equality expressing that the supremum over index set equals the zero weight space in the nilpotent context.

Русский

Существует равенство, выражающее равенство верхнего предела над индексами и нулевого весового пространства в нильпотентном контексте.

LaTeX

$$iSup (fun k => (⊥ : LieSubmodule R L M).ucs k) = genWeightSpace M (0 : L → R)$$

Lean4

theorem mem_posFittingCompOf (x : L) (m : M) : m ∈ posFittingCompOf R M x ↔ ∀ (k : ℕ), ∃ n, (toEnd R L M x ^ k) n = m :=
  by simp [posFittingCompOf]

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