span_le_span_iff — Mathlib

English

If a finite sum of vectors equals another, then the corresponding coefficients are equal componentwise for a linearly independent family.

Русский

Если конечная линейная комбинация векторов равна другой, то соответствующие коэффициенты равны компонентно для линейно независимой последовательности.

LaTeX

$$$\\text{LinearIndependent } R\\ v \\rightarrow \\forall f,g:\\, \\sum_i f_i v_i = \\sum_i g_i v_i \\Rightarrow \\forall i,\\ f_i=g_i$$$

Lean4

theorem span_le_span_iff [Nontrivial R] {s t u : Set M} (hl : LinearIndependent R ((↑) : u → M)) (hsu : s ⊆ u)
    (htu : t ⊆ u) : span R s ≤ span R t ↔ s ⊆ t :=
  ⟨le_of_span_le_span hl hsu htu, span_mono⟩

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