English
There exists a maximal set s of indices such that the family v restricted to s is linearly independent; moreover, any proper superset t ⊇ s that preserves independence must equal s.
Русский
Существует максимальное множество индексов s, на котором семейство v линейно независимо; если t ⊇ s и сохраняет независимость, то t = s.
LaTeX
$$$\\exists s:\\,\\mathrm{LinearIndepOn}_R(v,s) \\land \\forall t\\, (s\\subseteq t \\land \\mathrm{LinearIndepOn}_R(v,t) \\Rightarrow s=t)$$$
Lean4
/-- TODO : refactor to use `Maximal`. -/
theorem exists_maximal_linearIndepOn' (v : ι → M) :
∃ s : Set ι, (LinearIndepOn R v s) ∧ ∀ t : Set ι, s ⊆ t → (LinearIndepOn R v t) → s = t :=
by
let indep : Set ι → Prop := fun s => LinearIndepOn R v s
let X := { I : Set ι // indep I }
let r : X → X → Prop := fun I J => I.1 ⊆ J.1
have key : ∀ c : Set X, IsChain r c → indep (⋃ (I : X) (_ : I ∈ c), I) :=
by
intro c hc
dsimp [indep]
rw [linearIndepOn_iffₛ]
intro f hfsupp g hgsupp hsum
rcases eq_empty_or_nonempty c with (rfl | hn)
· rw [show f = 0 by simpa using hfsupp, show g = 0 by simpa using hgsupp]
haveI : IsRefl X r := ⟨fun _ => Set.Subset.refl _⟩
classical
obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
simpa using And.intro hfsupp hgsupp
exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI) g (subset_union_right.trans hI) hsum
have trans : Transitive r := fun I J K => Set.Subset.trans
obtain ⟨⟨I, hli : indep I⟩, hmax : ∀ a, r ⟨I, hli⟩ a → r a ⟨I, hli⟩⟩ :=
exists_maximal_of_chains_bounded
(fun c hc => ⟨⟨⋃ I ∈ c, (I : Set ι), key c hc⟩, fun I => Set.subset_biUnion_of_mem⟩) @trans
exact ⟨I, hli, fun J hsub hli => Set.Subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩
