linearIndepOn_iff_linearIndepOn_finset

English

Equivalent to the existence of two distinct finite-support coefficient functions witnessing a nontrivial relation on s.

Русский

Эквивалентно существованию двух различных коэффициентных функций с конечной поддержкой, дающих ненулевые линейные зависимости на s.

LaTeX

$$$\\\\neg \\\\mathrm{LinearIndepOn}_R(v,s) \\\\iff \\\\exists f,g : \ι \\to R, \\\\sum_{i \\\\in s} f(i) \\, v_i = \\\\sum_{i \\\\in s} g(i) \\, v_i \\\\\land \\\\exists i \\\\in s, f(i) \ne g(i).$$$

Lean4

theorem linearIndepOn_iff_linearIndepOn_finset : LinearIndepOn R v s ↔ ∀ t : Finset ι, ↑t ⊆ s → LinearIndepOn R v t
    where
  mp hv t hts := hv.mono hts
  mpr
    hv := by
    rw [LinearIndepOn, linearIndependent_iff_finset_linearIndependent]
    exact fun t ↦
      (hv (t.map <| .subtype _) (by simp)).comp (ι' := t) (fun x ↦ ⟨x, Finset.mem_map_of_mem _ x.2⟩) fun x ↦ by aesop

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