linear_independent vs span

Stream: general

[Scott Morrison]

Am I allowed to be upset that linear_independent takes an indexed family, while span takes a set?

[Scott Morrison]

Is there a better way to state

lemma linear_independent.fin_succ (n : ℕ) (ι : fin (n+1) → V)
  (hι : linear_independent K (ι ∘ fin.cast_succ))
  (hx : ι (fin.last n) ∉ span K (set.range (ι ∘ @fin.cast_succ n))) :
  linear_independent K ι :=

and does anyone have a proof that doesn't involved mucking about with sets too much? I would like this to be an easy consequence of the existing linear_independent.insert.

[Scott Morrison]

Or, to #xy this, if I'm planning on proving some vectors i : fin n \to V are linearly independent by inductively showing each initial segment of them are linearly independent, which lemmas am I meant to use to say this?

[Johan Commelin]

Scott Morrison said:

Am I allowed to be upset that linear_independent takes an indexed family, while span takes a set?

I think you are

[Reid Barton]

linear_independent has to be a family, while for span it doesn't matter so much.

[Johan Commelin]

linear_independent used to be a set, I think

[Johan Commelin]

Before the monster-refactor of linear algebra and finsupp, about a year ago