Linear independent equivalent formulations

Stream: Is there code for X?

[Martin Dvořák]

How can we prove that these two formulations of linear independence are equivalent?

import Mathlib

example {ι F : Type} [Field F] {S : Set ι} {f : ι → F} :
    LinearIndependent F (f · : S → F) ↔
    LinearIndependent F (fun x => x : S.image f → F) := by
  sorry

[Yaël Dillies]

They are not. Consider S := Set.univ, f := Function.const Bool 0

[Yaël Dillies]

The case that's true is given by docs#linearIndependent_image

[Martin Dvořák]

The awkward moment when you realize that Set.image actually produces a set.