linearIndependent_single_iff — Mathlib

English

An equivalence between Sigma-indexed singletons shows that the linear independence of the big map ix ↦ single ix.1 (f ix.1 ix.2) is equivalent to the family (f i) being linearly independent.

Русский

Эквивалентность между одиночными компонентами показывает, что линейная независимость главной карты эквивалентна линейной независимости семейства f_i.

LaTeX

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

Lean4

theorem linearIndependent_single_iff {φ : ι → Type*} {f : ∀ i, φ i → M} :
    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 _⟩

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