linearIndependent_single_iff — Mathlib

English

The linear independence of the map ix ↦ single ix.1 (f ix.1 ix.2) is equivalent to the family (f i) being collectively linearly independent; i.e., the big LI is equivalent to LI of each component.

Русский

Линейная независимость отображения ix ↦ single ix.1 (f ix.1 ix.2) эквивалентна тому, что семейство функций (f_i) линейно независимо совместно; то есть крупная LI эквивалентна LI каждой компоненты.

LaTeX

$$$\\text{LI}(R,\\, (\\!\\lambda ix. \\mathrm{single}_{ix.1}(f_{ix.1}(ix.2)))) \\iff \\forall i, \\text{LI}(R, f_i)$$$

Lean4

theorem linearIndependent_single_iff :
    LinearIndependent R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) ↔ ∀ i, LinearIndependent R (f i) :=
  ⟨fun h i ↦ (h.comp _ sigma_mk_injective).of_comp (lsingle i), linearIndependent_single _⟩

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