English
Let K be a division ring, V a K-vector space, and v: ι → V. If {v i : i ∈ s} is linearly independent and s ⊆ t, then there exists a subset b of t such that s ⊆ b, the vectors {v i : i ∈ t} lie in the span of {v i : i ∈ b}, and {v i : i ∈ b} is linearly independent.
Русский
Пусть K — делитривальное кольцо, V — векторное пространство над K, и задано v: ι → V. Если множество {v i : i ∈ s} линейно независимо и s ⊆ t, существует подмножество b ⊆ t такое, что s ⊆ b, векторная сумма {v i : i ∈ t} лежит в span{v i : i ∈ b}, и {v i : i ∈ b} линейно независимо.
LaTeX
$$$$\exists b \subseteq t,\ s \subseteq b \land v''t \subseteq \operatorname{span}_K(v''b) \land \text{LinearIndepOn }K\ v\ b,$$$$
Lean4
theorem exists_linearIndepOn_extension {s t : Set ι} (hs : LinearIndepOn K v s) (hst : s ⊆ t) :
∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ span K (v '' b) ∧ LinearIndepOn K v b :=
by
obtain ⟨b, sb, h⟩ :=
by
refine zorn_subset_nonempty {b | b ⊆ t ∧ LinearIndepOn K v b} ?_ _ ⟨hst, hs⟩
· refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
· exact sUnion_subset fun x xc => (hc xc).1
· exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2
· exact subset_sUnion_of_mem
refine ⟨b, h.prop.1, sb, fun _ ⟨x, hx, hvx⟩ => by_contra fun hn ↦ hn ?_, h.prop.2⟩
subst hvx
exact subset_span <| mem_image_of_mem v <| h.mem_of_prop_insert ⟨insert_subset hx h.prop.1, h.prop.2.insert hn⟩
