English
Given a finite t and LIOn on s with s ⊆ span t, there exists t' with t'⊆ s∪t, s⊆ t', and card(t') = card(t).
Русский
При конечном t и LIOn на s с s ⊆ span t существует t' ⊆ s∪t, s ⊆ t' и card(t') = card(t).
LaTeX
$$$$\exists t' : Finset V,\ ↑t' \subseteq s \cup \↑t \land s \subseteq ↑t' \land t'.card = t.card.$$$$
Lean4
theorem exists_of_linearIndepOn_of_finite_span {s : Set V} {t : Finset V} (hs : LinearIndepOn K id s)
(hst : s ⊆ (span K ↑t : Submodule K V)) : ∃ t' : Finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card := by
classical
have :
∀ t : Finset V,
∀ s' : Finset V,
↑s' ⊆ s →
s ∩ ↑t = ∅ →
s ⊆ (span K ↑(s' ∪ t) : Submodule K V) →
∃ t' : Finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card :=
fun t =>
Finset.induction_on t
(fun s' hs' _ hss' =>
have : s = ↑s' := eq_of_linearIndepOn_id_of_span_subtype hs hs' <| by simpa using hss'
⟨s', by simp [this]⟩)
fun b₁ t hb₁t ih s' hs' hst hss' =>
have hb₁s : b₁ ∉ s := fun h =>
by
have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
rwa [hst] at this
have hb₁s' : b₁ ∉ s' := fun h => hb₁s <| hs' h
have hst : s ∩ ↑t = ∅ :=
eq_empty_of_subset_empty <|
-- Porting note: `-subset_inter_iff` required.
Subset.trans (by simp [inter_subset_inter, -subset_inter_iff]) (le_of_eq hst)
Classical.by_cases (p := s ⊆ (span K ↑(s' ∪ t) : Submodule K V))
(fun this =>
let ⟨u, hust, hsu, Eq⟩ := ih _ hs' hst this
have hb₁u : b₁ ∉ u := fun h => (hust h).elim hb₁s hb₁t
⟨insert b₁ u, by simp [insert_subset_insert hust], Subset.trans hsu (by simp), by
simp [Eq, hb₁t, hb₁s', hb₁u]⟩)
fun this =>
let ⟨b₂, hb₂s, hb₂t⟩ := not_subset.mp this
have hb₂t' : b₂ ∉ s' ∪ t := fun h => hb₂t <| subset_span h
have : s ⊆ (span K ↑(insert b₂ s' ∪ t) : Submodule K V) := fun b₃ hb₃ =>
by
have : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : Set V) := by
simp only [insert_eq, union_subset_union, Subset.refl, subset_union_right, Finset.union_insert,
Finset.coe_insert]
have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) := span_mono this (hss' hb₃)
have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
simpa [insert_eq, -singleton_union, -union_singleton] using hss'
have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) := mem_span_insert_exchange (this hb₂s) hb₂t
rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃
let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset_iff, hb₂s, hs']) hst this
⟨u, Subset.trans hust <| union_subset_union (Subset.refl _) (by simp [subset_insert]), hsu, by
simp [eq, hb₂t', hb₁t, hb₁s']⟩
have eq : ((t.filter fun x => x ∈ s) ∪ t.filter fun x => x ∉ s) = t :=
by
ext1 x
by_cases x ∈ s <;> simp [*]
apply
Exists.elim
(this (t.filter fun x => x ∉ s) (t.filter fun x => x ∈ s) (by simp [Set.subset_def])
(by simp +contextual [Set.ext_iff]) (by rwa [eq]))
intro u h
exact ⟨u, Subset.trans h.1 (by simp +contextual [subset_def, or_imp]), h.2.1, by simp only [h.2.2, eq]⟩
