span_subset_span — Mathlib

English

If V = span(S), two linear maps f,g: V→N are equal iff they agree on S.

Русский

Если V = span(S), то линейные отображения равны тогда и только тогда, когда совпадают на S.

LaTeX

$$$f=g \iff \forall s\in S, f(s)=g(s)$ при $V=\operatorname{span} S$$$

Lean4

/-- A version of `Submodule.span_le_restrictScalars` with coercions. -/
@[simp]
theorem span_subset_span : ↑(span R s) ⊆ (span S s : Set M) :=
  span_le_restrictScalars R S s

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