English
There exists a maximal independent subset w.r.t. inclusion for the family v, with a universal property for supersets preserving independence.
Русский
Существует максимальная по включению независимая подмножество семейства v с универсальным свойством относительно расширений.
LaTeX
$$$\\exists s,\\mathrm{LinearIndepOn}_R(v,s) ∧ ∀ t \\ (s \\subseteq t ∧ \\mathrm{LinearIndepOn}_R(v,t) → s=t)$$$
Lean4
theorem exists_maximal_linearIndepOn (v : ι → M) :
∃ s : Set ι, (LinearIndepOn R v s) ∧ ∀ i ∉ s, ∃ a : R, a ≠ 0 ∧ a • v i ∈ span R (v '' s) := by
classical
rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
use I, hIlinind
intro i hi
specialize hImaximal (I ∪ { i }) (by simp)
set J := I ∪ { i } with hJ
have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
have hiJ : i ∈ J := by simp [J]
have h := by
refine mt hImaximal ?_
· intro h2
rw [h2] at hi
exact absurd hiJ hi
obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
have hfi : f i ≠ 0 := by
contrapose hIlinind
refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
rintro x hx
refine (memJ.mp (supp_f hx)).resolve_left ?_
rintro rfl
exact hIlinind (Finsupp.mem_support_iff.mp hx)
use f i, hfi
have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _), add_eq_zero_iff_eq_neg] at sum_f
rw [sum_f]
refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)
