mem_span_iff_of_fintype — Mathlib

English

If s is a subset with a Finite type structure, the membership in span_R s is equivalent to existence of a function f: s → R such that the finite sum over s of f(a)·a equals x.

Русский

Если s — подмножество, имеющее структуру конечного типа, то x ∈ span_R s эквивалентно существованию функции f: s → R cуммирования x = ∑_{a∈s} f(a)·a.

LaTeX

$$$x \in \operatorname{span}_R s \iff \exists f: s \to R, \sum_{a\in s} f(a) \cdot a = x$$$

Lean4

theorem mem_span_iff_of_fintype {s : Set M} [Fintype s] {x : M} : x ∈ span R s ↔ ∃ f : s → R, ∑ a : s, f a • a.1 = x :=
  by
  conv_lhs => rw [← Subtype.range_val (s := s)]
  exact mem_span_range_iff_exists_fun _

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