mem_ideal_smul_span_iff_exists_sum'

English

Same as above but with range f replaced by image f; equivalence holds.

Русский

То же самое, что и выше, но с образованием через image f.

LaTeX

$$$x \\in I \\cdot \\operatorname{span} (\\operatorname{image} f) \\iff \\exists a \\colon s \\to_R, a(i) \\in I, \\sum a(i) f(i) = x$$$

Lean4

theorem mem_ideal_smul_span_iff_exists_sum' {ι : Type*} (s : Set ι) (f : ι → M) (x : M) :
    x ∈ I • span R (f '' s) ↔ ∃ (a : s →₀ R) (_ : ∀ i, a i ∈ I), (a.sum fun i c => c • f i) = x := by
  rw [← Submodule.mem_ideal_smul_span_iff_exists_sum, ← Set.image_eq_range]

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