English
If v is a linearly independent family in M, then the directed supremum of the spans of the singleton vectors v_i is linearly independent.
Русский
Если семейство векторов v = (v_i) является линейно независимым в M, то направленный супремум (iSup) пространств-областей порождаемых этими векторами тоже линейно независимо.
LaTeX
$$$\\mathrm{LinearIndependent}_R(v) \\Rightarrow \\mathrm{iSupIndep}_{i}\\; R\\cdot v_i$$$
Lean4
/-- See also `iSupIndep_iff_linearIndependent_of_ne_zero`. -/
theorem iSupIndep_span_singleton (hv : LinearIndependent R v) : iSupIndep fun i => R ∙ v i :=
by
refine iSupIndep_def.mp fun i => ?_
rw [disjoint_iff_inf_le]
intro m hm
simp only [mem_inf, mem_span_singleton, iSup_subtype'] at hm
rw [← span_range_eq_iSup] at hm
obtain ⟨⟨r, rfl⟩, hm⟩ := hm
suffices r = 0 by simp [this]
apply hv.eq_zero_of_smul_mem_span i
convert hm
ext
simp
