sum_mem_iSup — Mathlib

English

If a finite collection f(i) ∈ p(i) for all i in a finite index set, then the sum ∑ f(i) belongs to the supremum ⨆ i, p(i).

Русский

Если для каждого i из конечного множества индексных элементов f(i) ∈ p(i), то сумма ∑ f(i) принадлежит верхнему объединению ⨆_i p(i).

LaTeX

$$$\\forall i, f(i) \\in p(i) \\Rightarrow \\sum_i f(i) \\in \\bigvee_i p(i)$$$

Lean4

theorem sum_mem_iSup {ι : Type*} [Fintype ι] {f : ι → M} {p : ι → Submodule R M} (h : ∀ i, f i ∈ p i) :
    (∑ i, f i) ∈ ⨆ i, p i :=
  sum_mem fun i _ ↦ mem_iSup_of_mem i (h i)

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