English
LinearIndepOn.extend is a construction that, given s ⊆ t, produces a subset b ⊆ t extending s, so that v''t lies in span of v''b and v restricted to b is linearly independent.
Русский
LinearIndepOn.extend строит новое подмножество b ⊆ t, содержащее s, такое что v''t ⊆ span(v''b) и {v i : i∈b} линейно независимо.
LaTeX
$$$$\text{extend}(hs,hst) := b\text{ with } b\subseteq t,\ s\subseteq b,\ v''t \subseteq \operatorname{span}_K(v''b),\ LinearIndepOn\ K\ v\ b.$$$$
Lean4
/-- `LinearIndepOn.extend` adds vectors to a linear independent set `s ⊆ t` until it spans
all elements of `t`. -/
noncomputable def extend (hs : LinearIndepOn K v s) (hst : s ⊆ t) : Set ι :=
Classical.choose (exists_linearIndepOn_extension hs hst)
