linearIndependent_iff_finset_linearIndependent

English

A family is linearly independent if and only if every finite subfamily is linearly independent.

Русский

Семейство линейно независимо тогда и только тогда, когда каждое конечное подсемейство линейно независимо.

LaTeX

$$$\\\\mathrm{LinearIndependent}_R(v) \\\\iff \\\\forall s : \\\\mathrm{Finset}\\\\iota, \\\\mathrm{LinearIndependent}_R(v \\\\circ (\\\\text{Subtype.val} : s \\\\to \\\\iota)).$$$

Lean4

/-- A family is linearly independent if and only if all of its finite subfamily is
linearly independent. -/
theorem linearIndependent_iff_finset_linearIndependent :
    LinearIndependent R v ↔ ∀ (s : Finset ι), LinearIndependent R (v ∘ (Subtype.val : s → ι)) :=
  ⟨fun H _ ↦ H.comp _ Subtype.val_injective, fun H ↦
    linearIndependent_iff'ₛ.2 fun s f g eq i hi ↦
      Fintype.linearIndependent_iffₛ.1 (H s) (f ∘ Subtype.val) (g ∘ Subtype.val)
        (by simpa only [← s.sum_coe_sort] using eq) ⟨i, hi⟩⟩

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