sum_mem_biSup — Mathlib

English

If a finite collection over a finite index set has each f(i) ∈ p(i), then the sum ∑_{i ∈ s} f(i) lies in ⨆ i ∈ s, p(i).

Русский

Если для каждого i в конечном наборе индексов f(i) ∈ p(i), то сумма ∑_{i ∈ s} f(i) принадлежит ⨆_{i ∈ s} p(i).

LaTeX

$$$\\forall i \\in s,\\; f(i) \\in p(i) \\Rightarrow \\sum_{i \\in s} f(i) \\in \\bigvee_{i \\in s} p(i)$$$

Lean4

theorem sum_mem_biSup {ι : Type*} {s : Finset ι} {f : ι → M} {p : ι → Submodule R M} (h : ∀ i ∈ s, f i ∈ p i) :
    (∑ i ∈ s, f i) ∈ ⨆ i ∈ s, p i :=
  sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_iSup_of_mem hi (h i hi)

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