Subset of LI family is LI

Stream: Is there code for X?

[Martin Dvořák]

I would like to prove that a subset of linearly-independent family is linearly-independent.
It must already exist in Mathlib, right?
I probably failed to write the statement in an idiomatic way.

import Mathlib

example {ι F : Type} [Field F] {I J : Set ι} (hIJ : I ⊆ J) {f : ι → F}
    (hJ : LinearIndependent F (f · : J → F)
      ) : LinearIndependent F (f · : I → F) :=
  sorry

[Edward van de Meent]

it looks very similar to docs#LinearIndependent.mono ?

[Martin Dvořák]

Thanks!

I will take it from here:

import Mathlib

example {F : Type} [Field F] {D E : Set F} (hIJ : D ⊆ E)
    (hJ : LinearIndependent F (Subtype.val : E → F)
      ) : LinearIndependent F (Subtype.val : D → F) :=
  LinearIndependent.mono hIJ hJ