mem_span_finset' — Mathlib

English

A variant of span finite-set representation using the same idea as mem_span_iff_of_fintype but with Finset indexing.

Русский

Вариант представления span для конечного множества, аналогичный mem_span_iff_of_fintype, с индексированием по Finset.

LaTeX

$$$x \in \operatorname{span}_R w \iff \exists n\,\exists f:\mathrm{Fin}\,n \to R, \exists g:\mathrm{Fin}\,n \to w, \sum_{i=0}^{n-1} f(i) \cdot g(i) = x$$$

Lean4

/-- A variant of `Submodule.mem_span_finset` using `s` as the index type. -/
theorem mem_span_finset' {s : Finset M} {x : M} : x ∈ span R s ↔ ∃ f : s → R, ∑ a : s, f a • a.1 = x :=
  mem_span_iff_of_fintype

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