linearIndepOn_of_finite — Mathlib

English

If a property holds for all finite subsets t ⊆ s that LinearIndepOn R v t, then LinearIndepOn R v s holds.

Русский

Если для всех конечных подмножеств t ⊆ s выполняется LinearIndepOn R v t, то LinearIndepOn R v s выполняется.

LaTeX

$$linearIndepOn_of_finite$$

Lean4

theorem linearIndepOn_of_finite (s : Set ι) (H : ∀ t ⊆ s, Set.Finite t → LinearIndepOn R v t) : LinearIndepOn R v s :=
  linearIndepOn_iffₛ.2 fun f hf g hg eq ↦
    linearIndepOn_iffₛ.1 (H _ (union_subset hf hg) <| (Finset.finite_toSet _).union <| Finset.finite_toSet _) f
      Set.subset_union_left g Set.subset_union_right eq

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