mem_of_span_eq_top_of_smul_pow_mem

English

A Finset-based version of a membership criterion using powers and smuls shows membership in a subalgebra when certain finitary relations hold.

Русский

Версия с FINSET для критерия принадлежности, использующая степени и умножения, демонстрирует принадлежность подпалгебре при соблюдении конечных условий.

LaTeX

$$$${s\\}' \\text{ и } {l}' \\text{ удовлетворяют соответствующим условиям, следовательно } x \\in S'$$$$

Lean4

theorem mem_of_span_eq_top_of_smul_pow_mem (s : Set S) (l : s →₀ S)
    (hs : Finsupp.linearCombination S ((↑) : s → S) l = 1) (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S)
    (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') : x ∈ S' :=
  mem_of_finset_sum_eq_one_of_pow_smul_mem S' l.support (↑) l hs (fun x => hs' x.2) hl x H

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