equivalence of two definitions of span

Stream: Is there code for X?

[Vasily Ilin]

I am used to thinking of a span of a set of vectors as the set of linear combinations over all (finite) subsets. In mathlib span is instead defined as the inf of all subpaces containing the set of vectors. Is there a lemma that shows the equivalence of these two definitions?
To be precise, I am looking for something like the following, at least when the set of vectors is finite.

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (n : ℕ) (v : fin n → V) (w : V) :
∃ f : fin n →₀ k,
w = finsupp.sum f (λ i s, s • v i) ↔ w ∈ submodule.span k (v '' (set.univ : set (fin n))) := sorry

[Damiano Testa]

Is docs#finsupp.mem_span_iff_total close to what you want?

[Kevin Buzzard]

@Vasily Ilin I was surprised to learn that in most cases where a human wants to start using linear combinations, thinking more abstractly will often enable you to just use the axioms of the closure operator instead. Are you sure you need this in your situation? The one exception is when proving things by induction but there are tailor-made induction procedures which help here rather than getting your hands dirty with finsupp

[Kevin Buzzard]

Ie can you un-XY your question? Closure/span is extremely functorial.

[Patrick Massot]

I agree with Kevin but it would still be nice to have this lemma. We have analogues for other closure operators. However using fin n is weird here, especially in combination with finsupp. Talking about function with finite support when the source type is finite is masochistic. Also there are missing parentheses around the existential quantifier. Vasily, you can prove the non-trivial implication in this lemma using docs#submodule.span_induction. And presumably you can also prove what you actually want to prove using that lemma (or something more abstract as Kevin wrote).

[Kevin Buzzard]

Oh yes the missing parens are a common gotcha -- right now this says the false statement "exists f, (P <-> Q)" instead of "(exists f, P) <-> Q"

[Vasily Ilin]

Kevin Buzzard said:

Ie can you un-XY your question? Closure/span is extremely functorial.

I don't know what "un-XY" means but I am trying to do the exercise in the image.
image.png
My attempt so far is below.

import tactic -- imports all the Lean tactics
import linear_algebra.basis

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (n : ℕ) (v : fin n → V) (lin_indep : linear_independent k v) (w : V) : linear_independent k (matrix.vec_cons w v) ↔ w ∉ submodule.span k (v '' (set.univ : set (fin n)))
:=
begin
  split,
  intros h hw,
  -- want to say that w is a linear combination of vectors in v, which implies that they are not linearly independent.
end

[Patrick Massot]

un-XY refers to #xy

[Patrick Massot]

and see docs#linear_independent_fin_succ'